proposition: Lemma extensionality_model_eq : CE -> exists V (M : interp V), extensional M /\ standard M /\ forall rho phi, Zeq phi -> rho ⊨ phi.
proof: Proof. intros ce. exists SET', (SET_interp' ce). split; try apply SET_ext'. split; try apply SET_standard'. intros rho phi []. - destruct H as [<-|[<-|[<-|[<-|H0]]]]; cbn; try congruence. now intros x x' y y' -> ->. now apply SET'_ZF'. - apply SET_sep'. 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)