∀ {α : Type u_1} {β : Type u_2} {P : α → Prop} {f : (a : α) → P a → β} {xs : List α} (H : ∀ a ∈ xs, P a),
  (List.pmap f xs H).head? =
    Option.map
      (fun x =>
        match x with
        | ⟨a, m⟩ => f a ⋯)
      xs.attach.head?