proposition: Lemma mem_head (x : A) xs : head x xs \in x :: xs.
proof: Proof. by case: xs=>[|y ys]; rewrite !inE //= eqxx orbT. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)