fact: Definition nf_rect : forall P : T1 -> Type, P zero -> (forall n: nat, P (cons zero n zero)) -> (forall a n b n' b', nf (cons a n b) -> P (cons a n b)-> lt b' (phi0 (cons a n b)) -> nf b' -> P b' -> P (cons (cons a n b) n' b')) -> forall a: T1, nf a -> P a.
imports: Coq(Arith Max Bool Lia Compare_dec Relations Ensembles Wellfounded Bool RelationClasses Operators_Properties ArithRing Logic.Eqdep_dec) hydras(More_Arith Restriction DecPreOrder) hydras(OrdNotations)