proposition: Theorem induction_ltof2T : forall P : A -> Type, (forall x : A, (forall y : A, ltof y x -> P y) -> P x) -> forall a : A, P a.
proof: Proof. exact (well_founded_induction_type A ltof well_founded_ltof). Defined.
imports: Coq(Lia) CoRN.stdlib_omissions.List Coq.Logic.Eqdep_dec Coq.Setoids.Setoid