no goals
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
a : α
l : List α
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
⊢ mapM f (a :: l) = do
    let __do_lift ← f a
    let __do_lift_1 ← mapM f l
    pure (__do_lift :: __do_lift_1)
simp [← mapM'_eq_mapM]