no goals
m : Type u_1 → Type u_2
α ε β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : m α
f : α → ExceptT ε m β
⊢ run (ExceptT.lift x >>= f) = do
    let a ← x
    run (f a)
simp[ExceptT.run, ExceptT.lift, bind, ExceptT.bind, ExceptT.mk, ExceptT.bindCont, map_eq_pure_bind]