proposition: Lemma step_S x b : noSubterm x b -> noLargeSubterm (S x) b.
proof: Proof. induction b; intros H. - split. + intros H'; noconf H'. + simpl. exact tt. - split. + intros H'; noconf H'. apply (fst H); reflexivity. + apply (IHb (snd H)). Qed.
imports: Equations(Equations) Below