proposition: Lemma SET_rep phi rho : rho ⊨ ax_rep phi.
proof: Proof. intros H x. cbn. exists (Srep (fun u v => (u .: (v .: rho)) ⊨ phi) x). intros y. rewrite repAx. - split; intros [z[H1 H2]]; exists z; split; trivial. + setoid_rewrite sat_comp. eapply sat_ext; try apply H2. now intros [|[]]. + setoid_rewrite sat_comp in H2. eapply sat_ext; try apply H2. now intros [|[]]. - intros a b b' H1 H2. apply (H a b b'); fold sat; eapply sat_comp, sat_ext. 2: apply H1. 3: apply H2. all: intros [|[]]; reflexivity. 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)