proposition: Lemma novar_abstr : forall (v : nat) (t : Term), NoLambdas t -> ~(HasVar v (abstr v t)).
proof: Proof. pose_hasvar. induction t; sauto. Reconstr.reasy (@Coq.Arith.PeanoNat.Nat.eqb_refl, @Coq.Bool.Bool.not_true_iff_false) Reconstr.Empty. Qed.
imports: Hammer(Reconstr) PeanoNat Omega