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