proposition: Lemma IB_N_e rho i n : rho i = n -> rho ⊨ N i -> mDN {m:nat | Num m = n}.
proof: Proof. intros Hrho H. destruct n as [m|a b]. * dn. now exists m. * intros H1. apply H; cbn -[dom_rel']. intros Hh. apply H1. rewrite Hrho in Hh. exfalso. apply (@h10_rel_irref (a,b) Hh). Qed.
imports: Undecidability.DiophantineConstraints(H10C) Undecidability.DiophantineConstraints.Util(H10UPC_facts) Undecidability.FOL(Utils.FriedmanTranslationFragment Syntax.Facts Deduction.FragmentNDFacts Semantics.Tarski.FragmentSoundness Semantics.Tarski.FragmentFacts Syntax.BinSig Semantics.Kripke.FragmentCore Semantics.Kripke.FragmentSoundness Semantics.Kripke.FragmentToTarski) Undecidability.Shared(Dec) Undecidability.Shared.Libs.PSL(Numbers) Coq(Arith Lia List) Undecidability.FOL.Reductions(H10UPC_to_FOL_constructions)