fact: Definition wf_QE_proj := forall i bc (bc_i := proj i bc), dnf_rterm bc -> qf_form bc_i && rformula bc_i.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)