proposition: Lemma iPr_spec rho' t t' d1 d2 : rho' t = d1 -> rho' t' = d2 -> rho' ⊨ Pr $t $t' <-> iPr d1 d2.
proof: Proof. cbn. intros -> ->. 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