proposition: Lemma term_eqP (T : eqType) : Equality.axiom (@term_eq T).
proof: Proof. move=> t1 t2; apply: (iffP idP) => [|<-]; last first. by elim: t1 {t2} => //= t -> // n; rewrite eqxx. elim: t1 t2. - by move=> n1 /= [] // n2 /eqP ->. - by move=> r1 /= [] // r2 /eqP ->. - by move=> n1 /= [] // n2 /eqP ->. - by move=> r1 hr1 r2 hr2 [] //= s1 s2 /andP [] /hr1 -> /hr2 ->. - by move=> r1 hr1 [] //= s1 /hr1 ->. - by move=> s1 hs1 n1 [] //= s2 n2 /andP [] /hs1 -> /eqP ->. - by move=> r1 hr1 r2 hr2 [] //= s1 s2 /andP [] /hr1 -> /hr2 ->. - by move=> r1 hr1 [] //= s1 /hr1 ->. - by move=> s1 hs1 n1 [] //= s2 n2 /andP [] /hs1 -> /eqP ->. Qed.
imports: HB(structures) mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq div choice fintype) mathcomp(bigop order ssralg finset fingroup zmodp) mathcomp(poly ssrnum)