∀ {m : Type u_1 → Type u_2} {ε : Type u_3} {σ α : Type u_1} [inst : Monad m] [inst_1 : MonadExceptOf ε m]
  (body : StateT σ m α) (handler : ε → StateT σ m α) (s : σ),
  (tryCatchThe ε body handler).run s = tryCatchThe ε (body.run s) fun x => (handler x).run s