proposition: Lemma Mem_map T T' (f : T -> T') x (s : seq T) : x \In s -> f x \In (map f s).
proof: Proof. elim: s=>[|y s IH] //; rewrite InE /=. by case=>[<-|/IH]; [left | right]. Qed.
imports: Coq(ssreflect ssrbool ssrfun Setoid) mathcomp(ssrnat seq eqtype) pcm(options)