∀ {α : Type u_1} {n : ℕ} {β : Type u_2} {xs : Array α} {h : xs.size = n} {P : α → Prop} {f : (a : α) → P a → β}
  {H : ∀ a ∈ Vector.mk xs h, P a}, Vector.pmap f (Vector.mk xs h) H = Vector.mk (Array.pmap f xs ⋯) ⋯