proposition: Lemma in_map_elim : forall x l, In x (map f l) -> exists y, In y l /\ x = f y.
proof: Proof. induction l; simpl; intros. contr. destruct H. exists a. auto. ded (IHl H). do 2 destruct H0. exists x0. auto. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)