proposition: Lemma eqslice_uniq s i : uniq s -> uniq (&=s i).
proof: Proof. rewrite /eq_slice; apply: slice_uniq. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext slice useqord)