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