proposition: Lemma sub_acc' L x : Acc (sub' L) x.
proof: Proof. Proof using HS2 HS1 HD. induction L. - constructor. intros y [_ [] ]. - apply sub_acc_step, IHL. 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