proposition: Lemma toNF_nf x: T1nf x -> toNF x = x.
proof: Proof. elim:x => //a Ha n b Hb /and3P [/Ha sa /Hb sb etc]. by rewrite /toNF -/toNF sa sb add_to_cons. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)