proposition: Lemma mem_map' : forall A B (l:list A) (f:A->B) (x:A) (y:B), mem x l -> y = f x -> mem y (map f l).
proof: Proof. Proof using. intros. subst. applys* mem_map. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)