proposition: Lemma nf_Acc : forall alpha, nf alpha -> Acc LT alpha.
proof: Proof. Proof nf_Wf. End well_founded. Definition transfinite_recursor_lt : forall (P:T1 -> Type), (forall x:T1, nf x -> (forall y:T1, nf y -> lt y x -> P y) -> P x) -> forall a, nf a -> P a. Proof. intros; eapply well_founded_restriction_rect; eauto; eexact nf_Wf;auto. Defined.
imports: Coq(Arith Lia Compare_dec Relations Wellfounded Wf_nat List Bool Eqdep_dec Ensembles ArithRing Logic) hydras(More_Arith Restriction DecPreOrder rpo.term rpo.rpo Epsilon0.T1)