proposition: Corollary indexall_uniq x s : uniq s -> indexall x s = if x \in s then [::index x s] else [::].
proof: Proof. by move=>U; apply: indexall_count1; rewrite (count_uniq_mem _ U) leq_b1. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)