proposition: Lemma SET'_ZF' rho : rho ⊫ ZF'.
proof: Proof. intros phi [<-|[<-|[<-|[<-|[<-|[<-|[<-|[]]]]]]]]; cbn. - intros X Y H1 H2. now apply Aczel_CE.set_ext. - now apply Aczel_CE.emptyE. - intros X Y Z. split; apply Aczel_CE.upairAx. - intros X Y. split; apply Aczel_CE.unionAx. - intros X Y. split; apply Aczel_CE.powerAx. - apply om_Ax1. - apply om_Ax2. 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)