Other rules related to C identifiers.
These are separate from the ones in atc-identifier-rules because these are only used in the new modular proof approach.
For now this is just one rule,
which serve to turn quoted integers into
Theorem:
(defthm omap-update-of-const-identifier (implies (and (syntaxp (quotep var)) (identp var)) (equal (omap::update var val scope) (omap::update (ident (ident->name var)) val scope))))