proposition: Lemma LS_setU_P 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 (LS_setU X f) <-> [/\ inc a X, pformula_in X h, pclosed h & pformula_valid_on X h] ).
proof: Proof. move => pa pb; split. by move /Zo_P => [pc pd]; move: (LS_setU_p1 pa pb pc) => [pe pf]; split. by move => [pc _ _ pd]; apply:Zo_i. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)