proposition: Corollary eqsl_notinL y b t s : t \notin s -> &=s (Interval (BSide b t) y) = [::].
proof: Proof. move=>T; apply: eqsl_overL=>/=. by rewrite (memNindex T); apply: leq_addr. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext slice useqord)