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