Update the Checked C specification to describe erasable syntax

[dtarditi]

The syntax modifications to allow macros to be used to erase Checked C annotations have been implemented in the compiler. They need to be added to the Checked C specification. Currently hey are only documented on a proposal page.