proposition: Lemma vars_transl2 : forall (t : Term) (n : nat), HasVar n t <-> HasVar n (transl2 t).
proof: Proof. pose_hasvar. induction t; sauto. - Reconstr.reasy (@vars_abstr2) Reconstr.Empty. - Reconstr.rsimple (@no_lams_transl2, @vars_abstr2, @novar_abstr2, @hs_lem) Reconstr.Empty. Qed.
imports: Hammer(Reconstr) PeanoNat Omega