proposition: Lemma LS_setU_p1 X f a (x:= (union (pfree_vars f))) (h:= (J (P f) ((Q f) +s1 (J x a)))): pformula_in X f -> (singletonp (pfree_vars f)) -> inc a X -> pformula_in X h /\ pclosed h.
proof: Proof. move => [[pa pb pc pd] pe] sf ax. have qa: (pfree_vars f) = singleton x. by rewrite /x; move:sf => [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). have da: (domain (Q f +s1 J x a)) = free_vars (P f). by rewrite domain_setU1 dfx. have ra: sub (range (Q f +s1 J x a)) X. rewrite range_setU1 => t /setU1_P; case; [ fprops | by move => ->]. have ha: pformula_in X (J (P f) (Q f +s1 J x a)). saw; saw; [fprops | by apply:fgraph_setU1 | ue]. by rewrite /pclosed /pfree_vars /h; aw; split => //;rewrite da setC_v. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)