simp [interpUB', Fitree.interpExcept] at *
case Vis
T : Type
E : Type → Type
R : Type
k : T → Fitree (UBE +' E) R
T✝ : Type
e✝ : sum1 UBE E T✝
k✝ : T✝ → Fitree (UBE +' E) T
ih :
  ∀ (a : T✝),
    interpUB' (Fitree.bind (k✝ a) k) =
      Fitree.bind (interpUB' (k✝ a)) fun x =>
        match x with
        | Except.error ε => Fitree.ret (Except.error ε)
        | Except.ok x => interpUB' (k x)
⊢ interpUB' (Fitree.bind (Fitree.Vis e✝ k✝) k) =
    Fitree.bind (interpUB' (Fitree.Vis e✝ k✝)) fun x =>
      match x with
      | Except.error ε => Fitree.ret (Except.error ε)
      | Except.ok x => interpUB' (k x)
case Vis
T : Type
E : Type → Type
R : Type
k : T → Fitree (UBE +' E) R
T✝ : Type
e✝ : sum1 UBE E T✝
k✝ : T✝ → Fitree (UBE +' E) T
ih :
  ∀ (a : T✝),
    Fitree.interp (Fitree.case UBE.handle Fitree.liftHandler) (Fitree.bind (k✝ a) k) =
      Fitree.bind (Fitree.interp (Fitree.case UBE.handle Fitree.liftHandler) (k✝ a)) fun x =>
        match x with
        | Except.error ε => Fitree.ret (Except.error ε)
        | Except.ok x => Fitree.interp (Fitree.case UBE.handle Fitree.liftHandler) (k x)
⊢ Fitree.interp (Fitree.case UBE.handle Fitree.liftHandler) (Fitree.bind (Fitree.Vis e✝ k✝) k) =
    Fitree.bind (Fitree.interp (Fitree.case UBE.handle Fitree.liftHandler) (Fitree.Vis e✝ k✝)) fun x =>
      match x with
      | Except.error ε => Fitree.ret (Except.error ε)
      | Except.ok x => Fitree.interp (Fitree.case UBE.handle Fitree.liftHandler) (k x)