fact: Hypothesis wf_QE_wproj : forall i bc (bc_i := wproj i bc), dnf_rterm (w_to_oclause bc) -> qf_form bc_i && rformula bc_i.
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)