proposition: Lemma select_nats k A: select (nats k) A = firstn k A.
proof: Proof. induction k in A |-*. - reflexivity. - destruct A. + rewrite select_nil; reflexivity. + cbn. rewrite select_S, IHk. reflexivity. Qed.
imports: List Arith Lia Undecidability.HOU(std.tactics std.lists.basics std.decidable)