Syntax-interp
Interpret a form on the syntactic representations of variables.
Logically, this always returns NIL. In FGL, this can be used when
under an unequiv congruence to examine the syntactic representation of
certain values and also to access and update the ACL2 state and FGL interpreter
state.