rfl
case Ret
E : Type → Type
ε : Type
F : Type → Type
T R : Type
h : E ~> ExceptT ε (Fitree F)
k : T → Fitree E R
r✝ : T
⊢ interpExcept h (bind (Ret r✝) k) =
    bind (interpExcept h (Ret r✝)) fun x? =>
      match x? with
      | Except.error ε_1 => ret (Except.error ε_1)
      | Except.ok x => interpExcept h (k x)
no goals