proposition: Lemma csubst_novar : forall (t s : Term) (v : nat), NoLambdas t -> ~(HasVar v t) -> csubst t v s = t.
proof: Proof. pose_hasvar. induction t; sauto. Reconstr.rsimple (@Coq.Arith.EqNat.beq_nat_true) Reconstr.Empty. Qed.
imports: Hammer(Reconstr) PeanoNat Omega