proposition: Lemma mem_headI (x : A) xs a : a = head x xs -> a \in x :: xs.
proof: Proof. by move=>->; apply: mem_head. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)