proposition: Lemma tuto_hasP_alt: 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. by case: (predU1P ysx) ax => [->|//]; rewrite ay. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finset)