proposition: Corollary slice_memE x s i : x \in &:s i = has (fun j => j \in i) (indexall x s).
proof: Proof. by rewrite /indexall -has_pred1; apply: slice_has. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext)