proposition: Lemma pformula_inst_p1 f (g := pformula_inst f): pformula f -> (singletonp (pfree_vars f)) -> [/\ pformula g, pclosed g , (forall X, pformula_in X f -> pformula_in X g) & forall X, pformula_valid_on X g -> nonempty (LS_setU X f)].
proof: Proof. move => [pa pb pc pd] pe; rewrite /pformula_inst. set x := union (pfree_vars f). have qa: (pfree_vars f) = singleton x. by rewrite /x; move:pe => [t ->]; rewrite setU_1. have dfx: domain (Q f) +s1 x = free_vars (P f). by move: qa; rewrite /pfree_vars => <-; rewrite (setU2_Cr pd). move:(set1_1 x); rewrite - qa /pfree_vars => /setC_P [fvp xdq1]. have va: variablep x by exact :((proj1 (free_vars_variables pb)) _ fvp). move:(free_vars_ex va pb); rewrite - qa /pfree_vars (setC_K pd). move:(proj1 (fkind_ex_p2 va pb)). set phi1 := (J val_ex (J x (P f))) => fp1 fv1. have clg: pclosed g. by rewrite /pclosed /pfree_vars /g /pformula_inst -/x; aw; rewrite fv1 setC_v. have pg: pformula g. have ff:=(proj1 (fkind_ex_p2 va pb)). rewrite /g /pformula /pformula_inst; aw; rewrite -/x fv1; split => //; fprops. have ph: forall X, pformula_in X f -> pformula_in X g. by move => X [sa sb]; split => //; rewrite /g /pformula_inst; aw. split => // X sb. move:(formula_val_ex X va pb) => [_ sc sd]. move /(pfree_vars_closed_pr X clg): sb. rewrite/g /pformula_inst; aw; rewrite -/x => /sd [se [g1 sf sg]]. rewrite -/phi1 in se sg; rewrite fv1 in sg. move :(formula_val_i pb sf) =>/gfunctions_P2 [fg1 dg1 rg1]. set a := Vg g1 x. have vaX: inc a X by apply: rg1; apply /(range_gP fg1); exists x => //; ue. set g2 := (Q f +s1 J x a). have gg: g1 = g2. by rewrite / g2 sg; symmetry; apply:setU1_restr => //; rewrite dg1. have ra:pformula_in X (J (P f) g1). saw; saw; fprops; rewrite dg1; fprops. have rb: pclosed (J (P f) g1). by rewrite /pclosed/pfree_vars; aw; rewrite dg1 setC_v. have rc: pformula_valid_on X (J (P f) g1). by apply /(proj2(pfree_vars_closed_pr X rb)); aw. by exists a; apply/Zo_P;split =>//; rewrite -/g2 - gg. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)