fact: Definition oclause_eq (T : eqType)(t1 t2 : oclause T) := let: Oclause eq_l1 neq_l1 lt_l1 leq_l1 := t1 in let: Oclause eq_l2 neq_l2 lt_l2 leq_l2 := t2 in [&& eq_l1 == eq_l2, neq_l1 == neq_l2, lt_l1 == lt_l2 & leq_l1 == leq_l2].
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)