proposition: Lemma nth_error_repeated (x: X) n k : k < n -> nth (repeat x n) k = Some x.
proof: Proof. intros H. erewrite repeated_tab, tab_map_nats, map_nth_error; eauto. now eapply nth_nats. Qed.
imports: List Arith Lia Undecidability.HOU(std.tactics std.lists.basics std.decidable)