simp only [mapM_empty, pure_bind]
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
x : Array α
a : α
⊢ (do
      let b ← f a
      let y ← mapM f #[]
      pure (cons b y)) =
    do
    let y ← mapM f #[]
    let b ← f a
    pure (push y b)
α : Type u
m : Type v → Type w
inst✝¹ : Monad m
β : Type v
inst✝ : LawfulMonad m
f : α → m β
x : Array α
a : α
⊢ (do
      let b ← f a
      pure (cons b #[])) =
    do
    let b ← f a
    pure (push #[] b)