proposition: Lemma eqsl_uR_rconsE s b k t : &=(rcons s k) (Interval (BSide b t) +oo) = if t \in s then rcons (&=s (Interval (BSide b t) +oo)) k else if b && (t == k) then [:: k] else [::].
proof: Proof. rewrite -cats1 eqsl_uR_catE /=; case: ifP=>//= _. - by rewrite cats1. by rewrite eqsl1_uR. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext slice useqord)