proposition: Lemma pmapS_filter s : map some (pmap s) = map f (filter [eta f] s).
proof: Proof. by elim: s => //= x s; case fx: (f x) => //= [u] <-; congr (_ :: _). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)