simp [h₁, h₂]
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)
α : Sort ?u.7562
β : Sort ?u.7563
f g : α → β
x y : α
h₁ : f = g
h₂ : x = y
⊢ f x = g y
no goals