proposition: Lemma has_predT_uslice (ks : seq A) i : uniq ks -> has predT (&=ks i) = has (fun z => index z ks \in ix_itv ks i) ks.
proof: Proof. move=>U; apply/hasP/hasP; case=>x. - by rewrite eqslice_mem_uniq // =>/andP [Hx Hi] _; exists x. by move=>Hx Hi; exists x=>//; rewrite eqslice_mem_uniq // Hx. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext slice useqord)