proposition: Lemma eqsl_oo_split t1 t2 (s1 s2 s : seq A) : t1 != t2 -> t1 \notin s1 -> t2 \notin s1 -> t2 \notin s -> &=(s1++t1::s++t2::s2) `]t1, t2[ = s.
proof: Proof. move=>N X1 X21 X2. rewrite eqsl_catE -cat_cons eqsl_uL_catE eqsl_catE /= eqsl_consE !eqsl_uL_consE eqsl_uR_consE /= !inE !eqxx /= !cats0. by rewrite (negbTE X1) (negbTE X21) eq_sym (negbTE N) /= (negbTE X2). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext slice useqord)