proposition: Lemma SET_sep' phi rho : rho ⊨ ax_sep phi.
proof: Proof. intros x. cbn. exists (sep ce (fun y => (y .: rho) ⊨ phi) x). intros y. rewrite Aczel_CE.sepAx. split; intros [H1 H2]; split; trivial. - setoid_rewrite sat_comp. eapply sat_ext; try apply H2. now intros []. - setoid_rewrite sat_comp in H2. eapply sat_ext; try apply H2. now intros []. 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)