proposition: Lemma sub_acc_cons' L x y : i_less y x -> Acc (sub' L) x -> Acc (sub' (y::L)) y.
proof: Proof. Proof using HS2 HS1 HD. intros H1 H2. apply sub_acc_cons; trivial. now apply (sub_acc_pred H1). 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