proposition: Lemma sub_acc_cons L x y : Acc (sub' L) x -> ~ i_less y x -> Acc (sub' (y::L)) x.
proof: Proof. Proof using HS2 HD. induction 1 as [x HX IH]. intros H. constructor. intros z [H1[->|H2] ]. - contradiction. - apply IH. 1: now split. intros HH. now eapply H, HS2 with z. 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