Hashconsed arrows/abstractions in the SMT encoding must be abstracted over their free variables

[mtzguido]

A bug and a fix in this PR, this was previously accepted:

let mk t = unit -> Dv t
let _ = assert (mk int == mk bool)

which is clearly pretty bad. The problem was that we were encoding the abstraction univ -> Dv t as a single fresh top-level SMT term, with a has computed from its definition. But, this fails to consider that a t is free in it, and therefore all mk _ calls are provably equal by the SMT. Abstractions had a similar issue.

The fix is to make these hashconsed terms dependent on their free variables, so the encoding of unit -> Dv t is now a Term to Term function. This is pretty simple and fixes the problem. Surprisingly there was only a single regressions in the examples.

This PR also removes the pre-typing axiom for impure functions, as we think it's probably not very useful.

[mtzguido]

Sadly this breaks HACL:

/home/guido/r/fstar/master/everest-TEMP/hacl-star/providers/evercrypt/fst/EverCrypt.DRBG.fst(70,14-78,17): (Error 276) queries-EverCrypt.DRBG-28.smt2: Unexpected output from Z3: (error "line 766902 column 0: unknown constant @x0")

looking at it.