rfl
case Ret
T R : Type
k : T → Fitree UBE R
r✝ : T
⊢ interpUB (Fitree.bind (Fitree.Ret r✝) k) =
    Fitree.bind (interpUB (Fitree.Ret r✝)) fun x =>
      match x with
      | Except.error ε => Fitree.ret (Except.error ε)
      | Except.ok x => interpUB (k x)
no goals