simp only [Except.bind]
ε α β : Type
f : α → Except ε β
a : β
x : α
⊢ (ok x).bind f = ok a ↔ ∃ b, ok x = ok b ∧ f b = ok a
ε α β : Type
f : α → Except ε β
a : β
x : α
⊢ f x = ok a ↔ ∃ b, ok x = ok b ∧ f b = ok a