∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {f : α → m β}
  {xs ys : Array α},
  Array.mapM f (xs ++ ys) = do
    let __do_lift ← Array.mapM f xs
    let __do_lift_1 ← Array.mapM f ys
    pure (__do_lift ++ __do_lift_1)