proposition: Lemma IB_rel_i rho 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) -> rho ⊨ rel ipl ipr ia ib ic id t.
proof: Proof. intros H. apply IB_P_i. intros a b Hpl Ha Hb. apply IB_P_i. intros c d Hpr Hc Hd Habcd. cbn -[dom_rel'] in Habcd. apply mDN_sat. intros Hc'. apply Habcd. intros Habcd'. apply Hc'. apply H. exists a,b,c,d. cbn in Habcd'. rewrite Hpl, Hpr in Habcd'. now repeat split. 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)