proposition: Lemma T1T2_inj n p : (n == p) = (T1T2 n == T1T2 p).
proof: Proof. elim: n p => //; first by case. move => a Ha n b Hb [] // a' n' b' /=. by rewrite T1eqE T2eqE - Ha - Hb eqxx. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)