proposition: Lemma valid_QE_proj e i : forall bc (bc_i := proj i bc) (ex_i_bc := ('exists 'X_i, odnf_to_oform [:: bc])%oT), dnf_rterm bc -> reflect (holds e ex_i_bc) (qf_eval e (proj i bc)).
proof: Proof. move=> bc; rewrite /dnf_rterm => hdnf; rewrite /proj; apply: (equivP idP). have -> : holds e ('exists 'X_i, odnf_to_oform [:: bc]) <-> (exists x : R, holds (set_nth 0 e i x) (odnf_to_oform (oclause_neq_leq_elim bc))). split; case=> x h; exists x; first by rewrite -oclause_neq_leq_elimP. by rewrite oclause_neq_leq_elimP. have -> : (exists x : R, holds (set_nth 0 e i x) (odnf_to_oform (oclause_neq_leq_elim bc))) <-> (exists x : R, holds (set_nth 0 e i x) (odnf_to_oform (map w_to_oclause (oclause_to_w bc)))). by split; case=> x; move/oclause_to_wP=> h; exists x. move: (dnf_rterm_subproof hdnf). rewrite /oclause_to_w; elim: (oclause_neq_leq_elim bc) => /= [|a l ih]. by split=> //; case. case/andP=> h1 h2; have {h2} ih := (ih h2); split. - case/orP. move/(valid_QE_wproj i e h1)=> /= [x /=] [] // [] h2 [] _ [] h3 _; exists x. by left. by case/ih => x h; exists x; right. - case=> x [] /=. + case=> h2 [] _ h3; apply/orP; left; apply/valid_QE_wproj => //=. by exists x; left. + by move=> hx; apply/orP; right; apply/ih; exists x. Qed.
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)