proposition: Lemma eqslice_mem (i : interval A) (ks : seq A) (k : A) : k \in &=ks i = has (fun j => j \in ix_itv ks i) (indexall k ks).
proof: Proof. by rewrite /eq_slice slice_memE. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext slice useqord)