proposition: Lemma nf_Wf : well_founded (restrict T1nf T1lt).
proof: Proof. have az: Acc (restrict T1nf T1lt) zero by split => y [_]; rewrite T1ltn0. elim;[ exact az | move => a Ha n b _]. elim:{a} Ha n b => a Ha Hb n b. case nx: (T1nf (cons a n b)); last by split => y [_ _]; rewrite nx. move/and3P: (nx);rewrite -/T1nf; move => [na nb lba]. have aca: Acc (restrict T1nf T1lt) a by split. have Hc: forall b, Acc (restrict T1nf T1lt) b -> T1nf (cons a 0 b)-> Acc (restrict T1nf T1lt) (cons a 0 b). move => c; elim => {} c qa qb qc; split; case; first by move => _; apply: az. move => a'' n'' b'' [] sa /= ua /and3P [_ nc _];move/and3P:(sa) => [ra rb _]. move: ua;case: (T1ltgtP a'' a) => ua ub. - by apply: Hb. - by case ub. - by move: ub sa; case ee:(n''==0); [rewrite ua (eqP ee) => ub; apply: qb | ]. have Hd: forall b, T1nf b -> b < phi0 a -> Acc (restrict T1nf T1lt) b. case; [by move => _ _ ; apply: az | move => a' n' b' nx']. rewrite phi0_lt1 => aa'. by apply: Hb; rewrite /restrict (T1nf_consa nx') na aa'. elim: n b {nb lba} (Hd _ nb lba) nx => [ // | n He b]; elim. move => c _ qb np; split; case; first by move => _; apply: az. move => a'' n'' b'' [sa /= sb _];move /and3P: (sa) => [ra rb rc]. move: sb; case: (T1ltgtP a'' a) => sc sb; [ by apply: Hb | by case sb |]. move: sb; case: (ltngtP n'' n.+1); [rewrite ltnS leq_eqVlt | done | move ->]. rewrite sc in rc; move => sb _; move: sa; case /orP: sb. move => /eqP ->; rewrite sc; apply: (He b'' (Hd _ rb rc)). move => qd qe. have nc0: T1nf (cons a n zero) by rewrite /= andbT. apply: (acc_rec (And3 qe _ nc0) (He _ az nc0)). by rewrite /= qd sc eqxx T1ltnn. move => sb; move/and3P: np => [pa pb pc]. rewrite sc;apply: (qb _ (And3 rb sb pb)); rewrite -sc //. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)