simp [mmap, mmap_append _ as as', LawfulMonad.pure_bind,
LawfulMonad.bind_assoc]
m : Type → Type
inst✝ : LawfulMonad m
α β : Type
f : α → m β
a : α
as as' : List α
⊢ mmap f (a :: as ++ as') = do
    let bs ← mmap f (a :: as)
    let bs' ← mmap f as'
    pure (bs ++ bs')
no goals