proposition: Lemma SET_standard' : standard SET_interp'.
proof: Proof. intros x. cbn. destruct (classof_ex ce x) as [s ->]. intros [n Hn] % classof_ele. exists n. rewrite <- Anumeral_numeral'. now apply classof_eq. 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)