proposition: Lemma vars_abstr2 : forall (t : Term) (n v : nat), n <> v -> (HasVar n t <-> HasVar n (abstr2 v t)).
proof: Proof. pose_hasvar. induction t; sauto. Reconstr.reasy (@Coq.Arith.EqNat.beq_nat_true) Reconstr.Empty. Qed.
imports: Hammer(Reconstr) PeanoNat Omega