proposition: Lemma select_map X Y (f: X -> Y) I A: map f (select I A) = select I (map f A).
proof: Proof. induction I in A |-*; cbn; eauto. rewrite nth_error_map_option. destruct nth; cbn; now rewrite IHI. Qed.
imports: List Arith Lia Undecidability.HOU(std.tactics std.lists.basics std.decidable)