proposition: Lemma pcformulas_inP X f: inc f (pcformulas_in X) <-> (pformula_in X f /\ pclosed f).
proof: Proof. split. move =>/Zo_P [pa [pb pc]]; split => //. by rewrite /pclosed /pfree_vars pc setC_v. move => [qa]. move:(qa) => [[pa pb pc pd] pe]. rewrite /pclosed /pfree_vars => /empty_setC pf. move: (extensionality pd pf) => pg. apply /Zo_i; [ apply/setX_P; split => // | by split]. apply/ sub_fgraphsP; exists (free_vars (P f)). by apply:(proj1 (free_vars_variables pb)). by apply/gfunctions_P2. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)