proposition: Lemma Acz_ZFeq' rho : rho ⊫ ZFeq'.
proof: Proof. intros phi [<-|[<-|[<-|[<-|[<-|[<-|[<-|[<-|[<-|[<-|[<-|[]]]]]]]]]]]]; cbn. - apply Aeq_ref. - apply Aeq_sym. - apply Aeq_tra. - intros s t s' t' -> ->. tauto. - apply Aeq_ext. - apply AEmptyAx. - intros X Y Z. apply AupairAx. - intros X Y. apply AunionAx. - intros X Y. apply ApowerAx. - apply AomAx1. - apply AomAx2. 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)