proposition: Lemma IB_erel_e rho ia ib ic id : rho ⊨ erel ia ib ic id -> exists a b 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 [pl [pr H]]. eapply IB_rel_e in H. destruct H as (a&b&c&d&Hpl&Hpr&Ha&Hb&Hc&Hd&Habcd1&Habcd2). exists a, b, c, d; now repeat split. 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