proposition: Lemma M_sep P x : (forall phi rho, rho ⊨ ax_sep phi) -> def_pred P -> exists y, forall z, z ∈ y <-> z ∈ x /\ P z.
proof: Proof. cbn. intros H [phi [rho Hp]]. destruct (H phi rho x) as [y H']; clear H. exists y. intros z. specialize (H' z). setoid_rewrite sat_comp in H'. rewrite (sat_ext _ _ (xi:=z.:rho)) in H'; try now intros []. firstorder. Qed.
imports: Undecidability.FOL(Syntax.Facts Semantics.Tarski.FullFacts ZF) Undecidability.FOL.Sets(ZF binZF) Undecidability.FOL.Sets.Models(Aczel Aczel_CE Aczel_TD) Coq(Lia)