proposition: Lemma step_N2 x y b : noSubterm y b -> noLargeSubterm (N x y) b.
proof: Proof. induction b; intros H. - split. + intros H'; noconf H'. + constructor. - split. + intros H'; noconf H'. apply (fst (fst H)); reflexivity. + split. * apply (IHb2 (snd (fst H))). * apply (IHb1 (snd (snd H))). Qed.
imports: Equations(Equations) Below