proposition: Lemma T1nf_rect (P : T1 -> Type): P zero -> (forall n: nat, P (cons zero n zero)) -> (forall a n b n' b', T1nf (cons a n b) -> P (cons a n b) -> b' < phi0 (cons a n b) -> T1nf b' -> P b' -> P (cons (cons a n b) n' b')) -> forall a, T1nf a -> P a.
proof: Proof. move =>H0 Hfinite Hcons; elim => // a IH1 n t IH2;case: a IH1. by rewrite T1nf_finite1; move => _ /eqP ->. move => a' n' c pa =>/and3P [pc pd pe]; auto. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)