proposition: Lemma Mem_cat x : forall s1 s2, (x \In s1 ++ s2) <-> x \In s1 \/ x \In s2.
proof: Proof. elim=>[|y s1 IH] s2 /=; first by split; [right | case]. rewrite !InE /=. split. - case=>[->|/IH]; first by left; left. by case; [left; right | right]. case; first by case; [left | move=>H; right; apply/IH; left]. by move=>H; right; apply/IH; right. Qed.
imports: Coq(ssreflect ssrbool ssrfun Setoid) mathcomp(ssrnat seq eqtype) pcm(options)