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.
