proposition: Lemma vars_transl2 : forall (t : Term) (n : nat), HasVar n t <-> HasVar n (transl2 t).
proof: Proof. induction t; qsimpl. - hauto using (@vars_abstr2). - hauto using (@no_lams_transl2, @vars_abstr2, @novar_abstr2, @hs_lem). Qed.
imports: Hammer(Tactics) Arith ZArith List Lia Hammer(Hints) Reals Lra Hammer(Reflect) Nat Psatz