proposition: Theorem nth_error_map : forall U (f : T -> U) ls n, nth_error (map f ls) n = match nth_error ls n with | None => None | Some x => Some (f x) end.
proof: Proof. induction ls; destruct n; simpl; auto. Qed.
imports: Coq.Lists.List Coq.Arith.PeanoNat