proposition: Lemma head_map {P Q} (f : P -> Q) z (s : seq P) : f (head z s) = head (f z) (map f s).
proof: Proof. by case: s. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)