This MR makes sure that no evidence related to calls to
iFresh is recorded in the proof term.
It's an alternative to the approach by @jtassaro in !224 (closed). Instead of using a let-binding in the context for the counter, this MR changes the sealing of
envs_entails so the counter can be changed using just the conversion rule. The advantage of this approach is that no additional information is printed to the user.