proposition: Lemma proj_satP : forall e f, reflect (holds e f) (proj_sat e f).
proof: Proof. move=> e f; have fP := quantifier_elim_rformP e (to_rform_rformula f). by apply: (iffP fP); move/to_rformP. 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)