Some events are generated in two slightly different variants:
one that is local to the generated encapsulate, and one that is exported from the encapsulate. Proof hints are in the former but not in the latter,
thus keeping the ACL2 history ``clean'';
some proof hints may refer to events
that are generated only locally to the encapsulate.
Some events are generated only locally to the generated encapsulate. These are auxiliary events
needed to introduce the non-local (i.e. exported) events,
but whose presence in the ACL2 history is no longer needed
once the exported events have been introduced.
These only-local events have generated fresh names.
In contrast, exported events have names
that are user-controlled, directly or indirectly.
