Make `iFresh` faster

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.

This MR gives a 3.48% speedup on lambdarust, see here. This is in the same ballpark as @jtassaro's version, which gives a 3.33% speedup on lambdarust, see here.