proposition: Corollary eqsl_uL_consL s b t : &=(t :: s) (Interval -oo (BSide b t)) = if b then [::] else [::t].
proof: Proof. by rewrite eqsl_uL_consE eqxx. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext slice useqord)