proposition: Lemma eqslice_mem_uniq (i : interval A) s (x : A) : uniq s -> x \in &=s i = (x \in s) && (index x s \in ix_itv s i).
proof: Proof. move=>U; rewrite eqslice_mem indexall_uniq //. by case: ifP=>//= _; rewrite orbF. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext slice useqord)