proposition: Lemma mem2r_cat {p1 p2 x y} : y \notin p2 -> mem2 (p1 ++ p2) x y = mem2 p1 x y.
proof: Proof. by move=> p2'y; rewrite mem2_cat (negPf p2'y) -orbA orbC andbF mem2rf. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)