proposition: Lemma IB_P_e rho p l r ip il ir c : rho ip = p -> rho il = l -> rho ir = r -> rho ⊨ P ip il ir c -> {a:nat & {b:nat & p = Pair a b /\ l = Num a /\ r = Num b}} -> rho ⊨ c.
proof: Proof. intros Hp Hl Hr H [a [b [Hp' [Hl' Hr']]]]. cbn in H. rewrite Hp, Hl, Hr, Hp', Hl', Hr' in H. cbn in H. apply H. - eapply IB_P'_i. now rewrite Hp, Hp'. - eapply IB_N_i. now rewrite Hl, Hl'. - eapply IB_N_i. now rewrite Hr, Hr'. - now destruct a. - easy. Qed.
imports: Undecidability.DiophantineConstraints(H10C) Undecidability.DiophantineConstraints.Util(H10UPC_facts) Undecidability.FOL(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) Undecidability.Shared(ListAutomation) Coq(Arith Lia List)