proposition: Lemma psub_equiv a b c d a' b' c' d' : a == a' -> b == b' -> c == c' -> d == d' -> psub a b c d -> psub a' b' c' d'.
proof: Proof. Proof using HE2 HE3 HER3. intros Ha Hb Hc Hd Habcd. induction Habcd as [c a b d Hac Hbd|d b a c Hdb Hac|c d a b Hac Hdb] in Ha,Hb,Hc,Hd,a',b',c',d'|-*. + eapply psub1. - now eapply HER3 with a c. - eapply HE3 with b. 1: now eapply HE2. now eapply HE3 with d. + eapply psub2. - now eapply HER3 with b d. - eapply HE3 with a. 1: now eapply HE2. now eapply HE3 with c. + eapply psub3. - now eapply HER3 with a c. - now eapply HER3 with b d. 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