proposition: Lemma nth_error_map_option n (f: X -> Y) (A: list X): nth_error (map f A) n = option_map f (nth_error A n).
proof: Proof. destruct (nth_error A n) eqn: H1. + eapply map_nth_error in H1. rewrite H1. reflexivity. + eapply nth_error_None in H1. eapply nth_error_None. now rewrite map_length. Qed.
imports: List Arith Lia Undecidability.HOU(std.tactics std.lists.basics std.decidable)