proposition: Corollary slice_uniq_memE x s i : uniq s -> x \in &:s i = (x \in s) && (bnd i.1 (size s) <= index x s < bnd i.2 (size s)).
proof: Proof. by move=>U; apply: slice_memE1; rewrite (count_uniq_mem _ U) leq_b1. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext)