proposition: Lemma mem2E s x y : mem2 s x y = subseq (if x == y then [:: x] else [:: x; y]) s.
proof: Proof. elim: s => [| h s]; first by case: ifP. rewrite mem2_cons => ->. do 2 rewrite inE (fun_if subseq) !if_arg !sub1seq /=. by have [->|] := eqVneq; case: eqVneq. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)