Antiquotations broken badly

[mtzguido]

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.