proposition: Lemma T2eqP : Equality.axiom T2eq.
proof: Proof. move=> x y; apply: (iffP idP) => [|<-]. elim: x y; first by case => [ // | a b n d//]. by move => a H1 b H2 n d H4;case => // a' b' n' d' /= /andP [/H1 ->] /andP [/H2 ->] /andP [/eqP -> /H4 ->]. by elim: x => // a Ha b Hb n d Hd; rewrite /= Ha Hb Hd eqxx. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)