fact: Hypothesis valid_QE_wproj : forall i bc (bc' := w_to_oclause bc) (ex_i_bc := ('exists 'X_i, odnf_to_oform [:: bc'])%oT) e, dnf_rterm bc' -> reflect (holds e ex_i_bc) (qf_eval e (wproj i bc)).
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)