proposition: Lemma M_rep R x : (forall phi rho, rho ⊨ ax_rep phi) -> def_rel R -> functional R -> exists y, M_is_rep R x y.
proof: Proof. Proof using VIEQ. intros H1 [phi [rho Hp]]. intros H2. cbn in H1. specialize (H1 phi rho). destruct H1 with x as [y Hy]. - intros a b b'. setoid_rewrite sat_comp. erewrite sat_ext. rewrite <- (Hp a b). 2: now intros [|[]]. erewrite sat_ext. rewrite <- (Hp a b'). 2: now intros [|[]]. rewrite VIEQ. apply H2. - exists y. intros v. split. + intros [u[U1 U2]] % Hy. exists u. split; trivial. setoid_rewrite sat_comp in U2. rewrite sat_ext in U2. rewrite (Hp u v). apply U2. now intros [|[]]; cbn. + intros [u[U1 U2]]. apply Hy. exists u. split; trivial. setoid_rewrite sat_comp. rewrite sat_ext. rewrite <- (Hp u v). apply U2. now intros [|[]]; cbn. 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)