proposition: Lemma HasP xs : Has xs <-> exists2 x, x \In xs & P x.
proof: Proof. elim: xs=>[|x xs IH] /=; first by split=>//; case. split. - case=>[H|/IH]; first by exists x=>//; rewrite InE; left. by case=>y H1 H2; exists y=>//; rewrite InE; right. case=>y; rewrite InE; case=>[->|H1 H2]; first by left. by right; apply/IH; exists y. Qed.
imports: Coq(ssreflect ssrbool ssrfun Setoid) mathcomp(ssrnat seq eqtype) pcm(options)