proposition: Lemma abstr2_correct : forall (t s : Term) (v : nat), NoLambdas t -> abstr2 v t @ s =w csubst t v s.
proof: Proof. pose_we. induction t; sauto. ycrush. assert (HH: forall b1 b2, (b1 || b2)%bool = false -> b1 = false /\ b2 = false). unfold orb; ycrush. pose proof occurs_spec. rewrite csubst_novar by ycrush. rewrite csubst_novar by ycrush. ycrush. Qed.
imports: Hammer(Reconstr) PeanoNat Omega