proposition: Lemma mem_seqP (A : eqType) x (s : seq A) : reflect (x \In s) (x \in s).
proof: Proof. elim: s=>[|y s IH]; first by constructor. rewrite inE; case: eqP=>[<-|H /=]; first by constructor; left. by apply: equivP IH _; rewrite InE; split; [right | case]. Qed.
imports: Coq(ssreflect ssrbool ssrfun Setoid) mathcomp(ssrnat seq eqtype) pcm(options)