no goals
m : Type u_1 → Type u_2
α ε β : Type u_1
e : ε
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → ExceptT ε m β
⊢ throw e >>= f = throw e
simp [throw, throwThe, MonadExceptOf.throw, bind, ExceptT.bind, ExceptT.bindCont, ExceptT.mk]