proposition: Lemma ierel_spec rho' a b c d da db dc dd : rho' a = da -> rho' b = db -> rho' c = dc -> rho' d = dd -> rho' ⊨ erel a b c d <-> ierel da db dc dd.
proof: Proof. intros H1 H2 H3 H4. unfold erel,rel,ierel. split. - intros [d1 [d0 H]]. exists d1,d0. rewrite <- !iPr_spec, <- !iP_spec. 1:apply H. all:easy. - intros [d1 [d0 H]]. exists d1,d0. rewrite <- !iPr_spec, <- !iP_spec in H. 1:apply H. all:easy. 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