proposition: Lemma mem_map : forall (A B:Type) (f:A->B) (l:list A) x, mem x l -> mem (f x) (map f l).
proof: Proof. Proof using. introv M. induction M; rew_listx; auto. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)