Identifier of a declarator.
A declarator always contains an identifier at its core. This function returns it, together with a companion function that operates on direct declarators, which is mutually recursive with the one for declarators.
Theorem:
(defthm return-type-of-declor->ident.ident (b* ((?ident (declor->ident declor))) (identp ident)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-dirdeclor->ident.ident (b* ((?ident (dirdeclor->ident dirdeclor))) (identp ident)) :rule-classes :rewrite)