proposition: Lemma nf_cons_cons a b c n a' b' c' n' d': T3nf (cons a b c n (cons a' b' c' n' d')) = [&& [a', b',c'] < [a, b,c], T3nf [a,b, c] & T3nf (cons a' b' c' n' d') ].
proof: Proof. simpl. case: (T3nf a);rewrite /= ?andbF //. case: (T3nf b);rewrite /= ? andbF //. case: (T3nf c);rewrite /= ? andbF //. by rewrite psi_lt1 andbC. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)