proposition: Lemma sub_acc_step L a x : Acc (sub' L) x -> Acc (sub' (a::L)) x.
proof: Proof. Proof using HS2 HS1 HD. induction 1 as [x HX IH]. constructor. intros y [H [->|H'] ]. - now apply (sub_acc_cons' H). - apply IH. now split. 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