fact: Definition lcons (L : clause) := (fF^+ \notin L) && [all s in L, if s is fV p^+ then fV p^- \notin L else true].
imports: Relations mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype)