proposition: Lemma vars_transl : forall (t : Term) (n : nat), HasVar n t <-> HasVar n (transl t).
proof: Proof. pose_hasvar. induction t; sauto. - Reconstr.reasy (@vars_abstr) Reconstr.Empty. - Reconstr.rsimple (@hs_lem, @vars_abstr, @novar_abstr, @no_lams_transl) Reconstr.Empty. Qed.
imports: Hammer(Reconstr) PeanoNat Omega