proposition: Lemma quantifier_elim_wf f : let qf := quantifier_elim f in rformula f -> qf_form qf && rformula qf.
proof: Proof. suffices aux_wf f0 n : let qf := elim_aux f0 n in rformula f0 -> qf_form qf && rformula qf. - by elim: f => //=; do ?[ move=> f1 IH1 f2 IH2; case/andP=> rf1 rf2; case/andP:(IH1 rf1)=> -> ->; case/andP:(IH2 rf2)=> -> -> // | move=> n f1 IH rf1; case/andP: (IH rf1)=> qff rf; rewrite aux_wf ]. rewrite /elim_aux => rf. suffices or_wf fs : let ofs := foldr Or False fs in all (@qf_form F) fs && all (@rformula F) fs -> qf_form ofs && rformula ofs. - apply: or_wf. suffices map_proj_wf bcs: let mbcs := map (proj n) bcs in all dnf_rterm bcs -> all (@qf_form _) mbcs && all (@rformula _) mbcs. by apply/map_proj_wf/qf_to_dnf_rterm. elim: bcs => [|bc bcs ihb] bcsr //= /andP[rbc rbcs]. by rewrite andbAC andbA wf_proj //= andbC ihb. elim: fs => //= g gs ihg; rewrite -andbA => /and4P[-> qgs -> rgs] /=. by apply: ihg; rewrite qgs rgs. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)