apply fequal2
case Vis
T R : Type
k : T → Fitree UBE R
T✝ : Type
e✝ : UBE T✝
k✝ : T✝ → Fitree UBE T
ih :
  ∀ (a : T✝),
    Fitree.interp UBE.handle (Fitree.bind (k✝ a) k) =
      Fitree.bind (Fitree.interp UBE.handle (k✝ a)) fun x =>
        match x with
        | Except.error ε => Fitree.ret (Except.error ε)
        | Except.ok x => Fitree.interp UBE.handle (k x)
fequal2 : ∀ (α : Sort ?u.7562) (β : Sort ?u.7563) (f g : α → β) (x y : α), f = g → x = y → f x = g y
⊢ (Fitree.bind (UBE.handle T✝ e✝) fun x =>
      match x with
      | Except.ok a => Fitree.interp UBE.handle (Fitree.bind (k✝ a) k)
      | Except.error e => Fitree.ret (Except.error e)) =
    Fitree.bind (UBE.handle T✝ e✝) fun x =>
      Fitree.bind
        (match x with
        | Except.ok a => Fitree.interp UBE.handle (k✝ a)
        | Except.error e => Fitree.ret (Except.error e))
        fun x =>
        match x with
        | Except.error e => Fitree.ret (Except.error e)
        | Except.ok x => Fitree.interp UBE.handle (k x)
case Vis.a
T R : Type
k : T → Fitree UBE R
T✝ : Type
e✝ : UBE T✝
k✝ : T✝ → Fitree UBE T
ih :
  ∀ (a : T✝),
    Fitree.interp UBE.handle (Fitree.bind (k✝ a) k) =
      Fitree.bind (Fitree.interp UBE.handle (k✝ a)) fun x =>
        match x with
        | Except.error ε => Fitree.ret (Except.error ε)
        | Except.ok x => Fitree.interp UBE.handle (k x)
fequal2 : ∀ (α β : Type 1) (f g : α → β) (x y : α), f = g → x = y → f x = g y
⊢ Fitree.bind (UBE.handle T✝ e✝) = Fitree.bind (UBE.handle T✝ e✝)

case Vis.a
T R : Type
k : T → Fitree UBE R
T✝ : Type
e✝ : UBE T✝
k✝ : T✝ → Fitree UBE T
ih :
  ∀ (a : T✝),
    Fitree.interp UBE.handle (Fitree.bind (k✝ a) k) =
      Fitree.bind (Fitree.interp UBE.handle (k✝ a)) fun x =>
        match x with
        | Except.error ε => Fitree.ret (Except.error ε)
        | Except.ok x => Fitree.interp UBE.handle (k x)
fequal2 : ∀ (α β : Type 1) (f g : α → β) (x y : α), f = g → x = y → f x = g y
⊢ (fun x =>
      match x with
      | Except.ok a => Fitree.interp UBE.handle (Fitree.bind (k✝ a) k)
      | Except.error e => Fitree.ret (Except.error e)) =
    fun x =>
    Fitree.bind
      (match x with
      | Except.ok a => Fitree.interp UBE.handle (k✝ a)
      | Except.error e => Fitree.ret (Except.error e))
      fun x =>
      match x with
      | Except.error e => Fitree.ret (Except.error e)
      | Except.ok x => Fitree.interp UBE.handle (k x)