∀ {α : Type u_1} {β : Type u_2} {P : α → Prop} (f : (a : α) → P a → β) (xs : Array α) (H : ∀ a ∈ xs, P a),
  Array.pmapImpl f xs H =
    Array.map
      (fun x =>
        match x with
        | ⟨x, h'⟩ => f x h')
      (xs.attachWith P H)