Typing preconditions in F* reflection typing judgment

[aseemr]

More of an F* issue, but since the main client of F* reflection typing is Pulse, and the F* change would require some churn in the Pulse checker, making an issue here.

In the typechecker callbacks to check equiv, subtyping, etc., we should require the caller to prove their typing. These calls are wired to the F* unifier that expects only well-typed F* terms.