proposition: Lemma sub_acc_pred L x y : i_less y x -> Acc (sub' L) x -> Acc (sub' L) y.
proof: Proof. Proof using HS2. intros H H'. constructor. intros z [H1 H2]. apply H'. split; trivial. now apply (HS2 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