∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {as : Array α} {f : α → m β}
  {p : Fin as.size → β → Prop},
  (∀ (i : Fin as.size), SatisfiesM (p i) (f as[i])) →
    SatisfiesM (fun arr => ∃ (eq : arr.size = as.size), ∀ (i : ℕ) (h : i < as.size), p ⟨i, h⟩ arr[i]) (Array.mapM f as)