proposition: Lemma head_notin (x y : A) xs : y \in xs -> x \notin xs -> head x xs != x.
proof: Proof. move=>Y X; apply/negP=>/eqP; move/(head_nilp X)/nilP=>E. by rewrite E in Y. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)