proposition: Lemma pfree_vars_closed_pr1 X x (V:= pformula_vals X x): pclosed x -> (V = \0c \/ V = \1c) /\ (V = \1c <-> inc (Q x) (formula_val X (P x))).
proof: Proof. rewrite /pclosed; move => h. have sv1: sub V \1c. rewrite /V/pformula_vals h gfunctions_empty; apply: Zo_S. have hb: inc emptyset \1c by rewrite /card_one; fprops. have sv2: V = \0c \/ V = \1c by move/setP_P: sv1; rewrite setP_1 => /set2_P. split => //; split => ha. have: inc emptyset V by rewrite ha. by move => /Zo_hi; rewrite setU2_0. have hc: inc emptyset V. apply /Zo_P; rewrite h gfunctions_empty setU2_0; split; fprops. by case sv2 => // hd; move: hc; rewrite hd; case; case. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)