proposition: Lemma T2finite2 x: T2finite x -> T2nf x -> x = \F ((T2split x).2).
proof: Proof. case: x => // a b n c; rewrite /T2finite => sa sb. rewrite (T2nf_finite sa sb) /T2split -/T2split sa. by move: sa => /eqP [] -> ->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)