proposition: Lemma size_induction X (f : X -> nat) (p : X -> Prop) : (forall x, (forall y, f y < f x -> p y) -> p x) -> forall x, p x.
proof: Proof. intros D x. apply D. revert x. enough (forall n y, f y < n -> p y) by eauto. intros n. induction n; intros y E. - exfalso; lia. - apply D. intros x F. apply IHn. lia. Qed.
imports: Undecidability.Shared.Libs.PSL.Prelim Lia