proposition: Lemma T1eqP : Equality.axiom T1eq.
proof: Proof. move=> n m; apply: (iffP idP) => [|<-]. elim: n m; first by case => [ // | a n b //]. move => a H1 n b H2 [] // a' n' b' /= /andP [/H1 -> /andP []]. by move => /eqP -> /H2 ->. by elim: n => // t ct n a caa /=;rewrite ct caa eqxx. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)