proposition: Lemma IB_P_i rho ip il ir l r : rho ip = Pair l r -> rho il = Num l -> rho ir = Num r -> rho ⊨ P ip il ir.
proof: Proof. cbn. intros Hp Hl Hr. rewrite !Hp, !Hl, !Hr. repeat split. - eapply IB_P'_i. exact Hp. - eapply IB_N_i. exact Hl. - eapply IB_N_i. exact Hr. Qed.
imports: Undecidability.DiophantineConstraints(H10C) Undecidability.DiophantineConstraints.Util(H10UPC_facts) Undecidability.FOL(Syntax.Facts Deduction.FullNDFacts Semantics.Tarski.FullSoundness Semantics.Tarski.FullFacts Syntax.BinSig) Undecidability.Shared(Dec) Undecidability.Shared.Libs.PSL(Numbers) Coq(Arith Lia List) Undecidability.Synthetic.Definitions