∀ {α : Type u_1} {q : α → Prop} {β : Type u_2} {l : List α} {p : { x // q x } → Prop} {f : (a : { x // q x }) → p a → β}
  (H₁ : ∀ x ∈ l, q x) (H₂ : ∀ a ∈ l.attachWith q H₁, p a),
  List.pmap f (l.attachWith q H₁) H₂ = List.pmap (fun a h => f ⟨a, ⋯⟩ ⋯) l ⋯