proposition: Lemma normaliser_model : CE -> TD -> exists V (M : interp V), extensional M /\ standard M /\ forall rho psi, ZF psi -> rho ⊨ psi.
proof: Proof. intros H1 H2. assert (inhabited extensional_normaliser) as [H] by now apply TD_CE_normaliser. exists SET, SET_interp. split; try apply SET_ext. split; try apply SET_standard. intros rho psi []. - now apply SET_ZF'. - apply SET_sep. - apply SET_rep. 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)