proposition: Lemma vars_transl : forall (t : Term) (n : nat), HasVar n t <-> HasVar n (transl t).
proof: Proof. induction t; qsimpl. - hauto using vars_abstr. - hauto use: @no_lams_transl, @vars_abstr, @novar_abstr, @hs_lem. Qed.
imports: Hammer(Tactics) Arith ZArith List Lia Hammer(Hints) Reals Lra Hammer(Reflect) Nat Psatz