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 Hc1 Hc3 Hc4 Hc5 Hpl Hpr. apply mDN_sat. intros Hc8. unshelve eapply (IB_P'_e (n:=rho ip) _ Hc3); [easy|]. intros [pa [pb Hp]]. unshelve eapply (IB_N_e (n:=rho il) _ Hc4); [easy|]. intros [la Ha]. unshelve eapply (IB_N_e (n:=rho ir) _ Hc5); [easy|]. intros [lb Hb]. apply Hpl; cbn -[dom_rel']; intros Hpl'. apply Hpr; cbn -[dom_rel']; intros Hpr'. rewrite Hp in *. rewrite <-Ha in *. rewrite <-Hb in *. unfold dom_rel' in *. apply Hc8. destruct la; eapply (Hc1 pa pb); congruence. 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)