proposition: Lemma oclause_eqP (T : eqType) : Equality.axiom (@oclause_eq T).
proof: Proof. move=> t1 t2; apply: (iffP idP) => [|<-] /=; last first. by rewrite /oclause_eq; case: t1=> l1 l2 l3 l4; rewrite !eqxx. case: t1 => [l1 l2 l3 l4]; case: t2 => m1 m2 m3 m4 /=; case/and4P. by move/eqP=> -> /eqP -> /eqP -> /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)