proposition: Lemma psub_acc p : Acc psub' p.
proof: Proof. Proof using HS2 HS1 HD HI HE1 HE2 HE3 HER3. destruct p as [x y]. revert y. induction (sub_acc x) as [x HX IHX]. intros y. induction (sub_acc y) as [y HY IHY]. constructor. intros [u v]. cbn. inversion 1; subst. - now apply IHX. - eapply (Morphisms_Prop.Acc_pt_morphism pequiv) with (x, v). + apply pequiv_equiv. + intros [a b] [a' b'] [Ha Hb] [c d] [c' d'] [Hc Hd]. split; apply psub_equiv; (try easy); apply HE2; easy. + now split. + apply IHY. easy. - now apply IHX. 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