∀ {m : Type u_1 → Type u_2} {ε α β : Type u_1} [inst : Monad m] (x : ExceptT ε m α) (f : α → ExceptT ε m β),
  (x >>= f).run = do
    let x ← x.run
    match x with
      | Except.ok x => (f x).run
      | Except.error e => pure (Except.error e)