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