cases x
ε α β : Type
x : Except ε α
f : α → Except ε β
a : β
⊢ x.bind f = ok a ↔ ∃ b, x = ok b ∧ f b = ok a
case error
ε α β : Type
f : α → Except ε β
a : β
a✝ : ε
⊢ (error a✝).bind f = ok a ↔ ∃ b, error a✝ = ok b ∧ f b = ok a

case ok
ε α β : Type
f : α → Except ε β
a : β
a✝ : α
⊢ (ok a✝).bind f = ok a ↔ ∃ b, ok a✝ = ok b ∧ f b = ok a