proposition: Lemma IB_P_i rho ip il ir c : (forall a b, rho ip = (Pair a b) -> rho il = (Num a) -> rho ir = (Num b) -> rho ⊨ c) -> rho ⊨ P ip il ir c.
proof: Proof. intros Hplrc. intros [pa [pb Hp]]%(IB_P'_e (n:=rho ip)) [la Ha]%(IB_N_e (n:=rho il)) [rb Hb]%(IB_N_e (n:=rho ir)) Hpl Hpr. 2-4: easy. cbn in Hpl, Hpr. rewrite Hp,<-Ha,<-Hb in *. apply (@Hplrc la rb); destruct la; congruence. 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)