∀ (α : Type u_2) (β : Type u_1) (p : α → Prop) (f : (a : α) → p a → β) (l' : List α) (hL' : ∀ ⦃x : α⦄, x ∈ l' → p x),
  List.pmap f l' hL' =
    List.map
      (fun x =>
        match x with
        | ⟨x, hx⟩ => f x hx)
      (List.pmap Subtype.mk l' hL')