proposition: Lemma tuto_hasP : forall (a : pred T) s, reflect (exists2 x, x \in s & a x) (has a s).
proof: Proof. move=> a; elim=> [|y s IHs] /=; first by right; case. case ay: (a y); first by left; exists y; rewrite ?mem_head. apply: (iffP IHs) => [] [x ysx ax]; exists x => //; first exact: mem_behead. Search _ (_ \in cons _ _). by move: ysx ax; rewrite in_cons; case/orP=> //; move/eqP->; rewrite ay. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finset)