induction t with
| Ret _ => rfl
| Vis _ _ ih =>
    simp [interpUB', Fitree.interpExcept] at *
    simp [Fitree.interp, Fitree.bind, Bind.bind]
    simp [ExceptT.bind, ExceptT.mk, ExceptT.bindCont]
    have fequal2 α β (f g: α → β) x y: f = g → x = y → f x = g y :=
      fun h₁ h₂ => by simp [h₁, h₂]
    apply fequal2; rfl; funext x
    cases x <;> simp [ih]
T : Type
E : Type → Type
R : Type
t : Fitree (UBE +' E) T
k : T → Fitree (UBE +' E) R
⊢ interpUB' (Fitree.bind t k) =
    Fitree.bind (interpUB' t) fun x =>
      match x with
      | Except.error ε => Fitree.ret (Except.error ε)
      | Except.ok x => interpUB' (k x)
no goals