proposition: Lemma lt_wf_rect : forall (p : nat) (P : nat -> Type), (forall n : nat, (forall m : nat, m < n -> P m) -> P n) -> P p.
proof: Proof. exact (fun (p : nat) (P : nat -> Type) (F : forall n : nat, (forall m : nat, m < n -> P m) -> P n) => induction_ltof2T nat (fun m : nat => m) P F p). Defined.
imports: Coq(Lia) CoRN.stdlib_omissions.List Coq.Logic.Eqdep_dec Coq.Setoids.Setoid