proposition: Lemma complete_induction (p : nat -> Prop) (x : nat) : (forall x, (forall y, y<x -> p y) -> p x) -> p x.
proof: Proof. intros H. apply (@size_induction nat id p H x). Qed.
imports: Undecidability.Shared.Libs.PSL.Prelim Lia