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