proposition: Lemma appears_in_app (xs ys : seq X) (x:X): appears_in x (xs ++ ys) = appears_in x xs || appears_in x ys.
proof: Proof. elim: xs=>//= a ls Hi. case: (a == x). by simpl. by []. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype seq)