fact: Definition lt_of_oclause (R : Type) (x : oclause R) := let: Oclause _ _ y _ := x in y.
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)