∀ {α : Type u_1} {β : Type u_2} {γ : Type v} {m : Type v → Type w} [inst : Monad m] [LawfulMonad m] {f : α → β → m γ}
  {as : Array α} {bs : Array β}, Array.zipWithM f as bs = Array.mapM id (Array.zipWith f as bs)