proposition: Lemma eqsl_consE s k b1 t1 b2 t2 : &=(k :: s) (Interval (BSide b1 t1) (BSide b2 t2)) = if t1 == k then if t2 == k then if b1 && ~~ b2 then [::k] else [::] else if b1 then k :: &=s (Interval -oo (BSide b2 t2)) else &=s (Interval -oo (BSide b2 t2)) else if t2 == k then [::] else &=s (Interval (BSide b1 t1) (BSide b2 t2)).
proof: Proof. rewrite -cat1s eqsl_catE /= !inE. case: eqVneq=>[{t1}->|N1]; case: eqVneq=>[E2|N2] //=. - by rewrite /eq_slice /= E2 eqxx; case: b1; case: b2. by rewrite /eq_slice /= eqxx; case: b1. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext slice useqord)