proposition: Lemma findallE p s : findall p s = unzip1 (filter (p \o snd) (zip (iota 0 (size s)) s)).
proof: Proof. rewrite /findall. move: (@findall_auxE (id, 0) p s)=>/= /(_ (fun s1 s2 : seq nat => erefl)). case E: (findall_aux (id, 0) p s)=>[rs ix] /=; case=>/(_ [::]) -> _. by rewrite cats0. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)