proposition: Lemma nth_error_lt_Some Z m (L: list Z): m < length L -> exists a, nth L m = Some a.
proof: Proof. intros H % nth_error_Some. destruct nth; intuition idtac. now (exists z). Qed.
imports: List Arith Lia Undecidability.HOU(std.tactics std.lists.basics std.decidable)