proposition: Lemma IB_rel_e rho ipl ipr ia ib ic id t : rho ⊨ rel ipl ipr ia ib ic id t -> {a&{b&{c&{d|rho ipl=Pair a b /\ rho ipr = Pair c d /\ rho ia=Num a /\ rho ib=Num b /\ rho ic=Num c /\ rho id=Num d /\ h10upc_sem_direct ((a,b),(c,d))}}}} -> rho ⊨ t.
proof: Proof. intros H [a [b [c [d [Hpl [Hpr [Ha [Hb [Hc [Hd Habcd]]]]]]]]]]. unfold rel in H. eapply IB_P_e in H; cbn. 2-4: reflexivity. 2: eexists; eexists; repeat split; eassumption. eapply IB_P_e in H; cbn. 2-4: reflexivity. 2: eexists; eexists; repeat split; eassumption. cbn in H. apply H. dn. rewrite Hpl, Hpr. easy. 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)