proposition: Lemma nth_map_some : forall (l : list A) i (f: A -> A) a, nth_error l i = Some a -> nth_error (map f l) i = Some (f a).
proof: Proof. induction l. destruct i; intros; discr. intros i f a'. destruct i; simpl. intro aa'; inversion aa'; trivial. apply IHl. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)