proposition: Lemma mem2_cat p1 p2 x y : mem2 (p1 ++ p2) x y = mem2 p1 x y || mem2 p2 x y || (x \in p1) && (y \in p2).
proof: Proof. rewrite [LHS]/mem2 index_cat fun_if if_arg !drop_cat addKn. case: ifPn => [p1x | /mem2lf->]; last by rewrite ltnNge leq_addr orbF. by rewrite index_mem p1x mem_cat -orbA (orb_idl (@mem2r _ _ _)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)