proposition: Lemma IB_rel_e rho ipl ipr ia ib ic id : rho ⊨ rel ipl ipr ia ib ic id -> {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))}}}}.
proof: Proof. intros [[H1 H2] H3]. eapply IB_P_e in H1, H2. 2-7: reflexivity. destruct H1 as (a&b&Hpl&Ha&Hb), H2 as (c&d&Hpr&Hc&Hd). exists a, b, c, d; repeat split; try easy. all: cbn in H3; rewrite Hpl, Hpr in H3; lia. 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