proposition: Lemma ierel_spec' rho' a b c d : rho' ⊨ erel a b c d <-> ierel (rho' a) (rho' b) (rho' c) (rho' d).
proof: Proof. now apply ierel_spec. 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