proposition: Lemma eqseq_pivotr x s1 s2 s3 s4 : x \notin s3 -> x \notin s4 -> (s1 ++ x :: s2 == s3 ++ x :: s4) = (s1 == s3) && (s2 == s4).
proof: Proof. by move=> *; rewrite eq_sym eqseq_pivotl//; case: eqVneq => /=. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)