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