proposition: Lemma pformula_vals_aux X x g: pformula_in X x -> inc g (gfunctions (pfree_vars x) X) -> inc (Q x \cup g) (formula_values X (P x)).
proof: Proof. move => [[pa pb pc pd] pe] /gfunctions_P2 [pf pg ph]. apply/gfunctions_P2; split. + apply: fgraph_setU2 => //; rewrite pg /pfree_vars; apply: set_I2Cr. + by rewrite domain_setU2 pg /pfree_vars setU2_C; apply/setCU_K. + rewrite range_setU2 => t/setU2_P; case; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)