Some fixes/improvements to the core typechecker

[mtzguido]

Most importantly:

• Core/Tactics: controlling SMT guards and unfolding for check_equiv: this adds a new flag to the check_equiv invocation to forbid it from generating guards and unfolding definitions. I plan to use it from Pulse to match vprops.

• Core.check_equiv: always WHNF: adding some normalization to always work with terms in HNF. This makes matching, for example, 1+2 and 3 trivial.

• Core: allow checking pure/ghost (non-Tot) lets: talked about with @nikswamy. The first call to check lb.lbdef will accumulate a guard for the precondition if need be, and similarly for the body, so this should be safe. What we are not doing is using the spec of the lbdef to weaken the guard of the body. To do that I think we would need to obtain the strongest post of the lbdef, and we don't have machinery for that. I wonder if instead of accumulating guards Core could accumulate a WP of the checked term, in which case this would just be WP composition, and at the top-level we would instantiate with the fun _ -> True postcondition. In any case, it doesn't seem like a limitation in the tests I'm doing, and it is sound.

• Core: fix checking of letbinding: fix the type in the subtyping call, it was off by one level.

• Tactics: exposing full check_equiv with both flags: the check_equiv tactic is now derived from the t_check_equiv primitive which provides access to both flags. check_equiv_nosmt is defined to set both flags to false. This will require a small Pulse patch since the snapshot has fully resolved names.

[nikswamy]

Thanks @mtzguido

I reviews the core changes and they look good to me.

I agree that we could weaken the guard as an additional improvement in the future, but it's sound to not do that. So, I'm okay with it as is for now.

[mtzguido]

Thanks for reviewing! Merging.