Antiquotations broken badly

```fstar
module VerifiedTransform

open FStar.Tactics.V2
open FStar.Reflection.Typing

let t_unit = `()

let mk_eq2 (ty t1 t2 : term) : Tot term =
(`squash (eq2 #(`#ty) (`#t1) (`#t2)))

let valid (g:env) (phi:term) : prop =
squash (typing g t_unit (E_Total, mk_squash phi))

let test (g t0 t1 t2 ty : _) =
assume (valid g (mk_eq2 ty t0 t1));
assert (valid g (mk_eq2 ty t0 t2));
()
```
The last test should not succeed. My guess is that somehow the SMT thinks that these two terms (`mk_eq2 ty t0 t1` and `mk_eq2 ty t0 t2`) are equal, but clearly they are not.