proposition: Lemma hasP {a s} : reflect (exists2 x, x \in s & a x) (has a s).
proof: Proof. elim: s => [|y s IHs] /=; first by right; case. exact: equivP (orPP idP IHs) (iff_sym exists_cons). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)