proposition: Lemma T3finite2 x: T3finite x -> T3nf x -> x = \F ((T3split x).2).
proof: Proof. case: x => // a b c n d; rewrite /T3finite => sa sb. rewrite (T3nf_finite sa sb) /T3split -/T3split sa. by move: sa => /and3P [/eqP -> /eqP -> /eqP ->]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)