proposition: Lemma MapP T1 T2 (f : T1 -> T2) (s : seq T1) (y : T2) : y \In map f s <-> exists2 x, x \In s & y = f x.
proof: Proof. elim: s => [|x s IHs] /=; first by split=>//; case. rewrite In_cons; split. - case=>[->|]; first by exists x=>//; apply/In_cons; left. by case/IHs=>k H ->; exists k=>//; apply/In_cons; right. case=>k /In_cons [->|H E]; first by left. by right; apply/IHs; exists k. Qed.
imports: Coq(ssreflect ssrbool ssrfun Setoid) mathcomp(ssrnat seq eqtype) pcm(options)