proposition: Lemma select_nil I: select I nil = nil.
proof: Proof. induction I; cbn. - reflexivity. - destruct nth eqn: H; eauto. eapply nth_error_In in H; cbn in H; intuition easy. Qed.
imports: List Arith Lia Undecidability.HOU(std.tactics std.lists.basics std.decidable)