proposition: Lemma phi_inj1 a b b': T2nf b -> T2nf b' -> (phi a b == phi a b') = (b == b').
proof: Proof. move => nb nb'; case bb:(b== b'); first by rewrite (eqP bb) eqxx. by apply /negP => /eqP /(phi_inj nb nb') => /eqP; rewrite bb. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)