proposition: Lemma indexall_count1 x s : count_mem x s <= 1 -> indexall x s = if x \in s then [::index x s] else [::].
proof: Proof. by rewrite /indexall /index -has_pred1; apply: findall_count1. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)