proposition: Lemma map_nilP {B : eqType} (f : B -> A) s : reflect (exists k, k \in map f s) (map f s != [::]).
proof: Proof. case: has_nilP=>X; constructor. - by case/hasP: X=>x; exists x. by case=>k K; elim: X; apply/hasP; exists k. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)