proposition: Lemma SET_standard : standard SET_interp.
proof: Proof. intros x. cbn. destruct x. unfold Som, NS, IN. cbn. rewrite <- (CR1 Aom). intros [n Hn]. exists n. rewrite <- Anumeral_numeral. now apply Aeq_p1_NS_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)