proposition: Lemma indexall_head x s : index x s = head (size s) (indexall x s).
proof: Proof. by rewrite /index /indexall findall_head. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)