proposition: Lemma wf_QE_proj i : forall bc (bc_i := proj i bc), dnf_rterm bc -> qf_form bc_i && rformula bc_i.
proof: Proof. case=> leq lneql llt lle /= hdnf; move: (hdnf). rewrite /dnf_rterm /=; case/and4P=> req rneq rlt rle; rewrite /proj; apply/andP. move: (dnf_rterm_subproof hdnf). elim: (oclause_to_w _ ) => //= [a t] ih /andP [h1 h2]. by case: (ih h2)=> -> ->; case/andP: (wf_QE_wproj i h1) => -> ->. 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)