proposition: Lemma nth_error_map : forall (A B : Set) (f : A -> B) (l : list A) i, match nth_error (map f l) i with | Some f_li => match nth_error l i with | Some li => f_li = f li | None => False end | None => match nth_error l i with | Some li => False | None => True end end.
proof: Proof. induction l as [ | a l ]; intro i; destruct i as [ | i ]; simpl; trivial. apply IHl; trivial. Qed.
imports: List Arith