proposition: Lemma pformulas_inP X f: inc f (pformulas_in X) <-> pformula_in X f.
proof: Proof. split; [by move /Zo_hi | move => h; apply /Zo_i => //]. move:h => [[pa pb pc pd] pe]. apply /setX_P; split => //. apply/ sub_fgraphsP; exists (domain (Q f)). by apply: (sub_trans pd); apply:(proj1 (free_vars_variables pb)). by apply/gfunctions_P2. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)