proposition: Lemma sub_acc x : Acc (fun a b => i_less a b) x.
proof: Proof. Proof using HS2 HS1 HD. destruct HD as [L HL]. induction (sub_acc' L x) as [x _ IH]. constructor. intros y H. now apply IH. 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