proposition: Lemma mem2lr_splice {p1 p2 p3 x y} : x \notin p2 -> y \notin p2 -> mem2 (p1 ++ p2 ++ p3) x y = mem2 (p1 ++ p3) x y.
proof: Proof. move=> p2'x p2'y; rewrite catA !mem2_cat !mem_cat. by rewrite (negPf p2'x) (negPf p2'y) (mem2lf p2'x) andbF !orbF. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)