proposition: Lemma appears_in_appP (xs ys : seq Y) (x:Y): appears_inP x (xs ++ ys) <-> appears_inP x xs \/ appears_inP x ys.
proof: Proof. split; elim: xs=>[| a ls Hi]. - by right. - rewrite cat_cons; case. - by left; left. by case/Hi; [left|]; right. - by rewrite cat0s; case. by case=>//=; intuition. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype seq)