m : Type u_1 → Type u_2
α β ε : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β
x : ExceptT ε m α
⊢ x >>= pure ∘ f = f <$> x
m : Type u_1 → Type u_2
α β ε : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β
x : ExceptT ε m α
⊢ x >>= pure ∘ f = f <$> x
intros
no goals
m : Type u_1 → Type u_2
α β ε : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β
x : ExceptT ε m α
⊢ x >>= pure ∘ f = f <$> x
rfl