proposition: Lemma P_drv x y : i_P x y -> exists s t, derivable R s t /\ x == ienc s /\ y == ienc t.
proof: Proof. Proof using HS2 HS1 HI HD HE1 HE2 HE3 HER1 HER3. apply P_drv' with (p:=(x,y)). Qed.
imports: Lia Arith Undecidability.PCP.PCP Undecidability.PCP.Util.PCP_facts Undecidability.Synthetic.DecidabilityFacts Undecidability(FOL.Utils.FullSyntax) Undecidability(FOL.FSAT) Undecidability.Shared.ListAutomation