induction t with
| Ret _ => rfl
| Vis _ _ ih =>
    simp [interpExcept] at *
    simp [interp, 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]
E : Type → Type
ε : Type
F : Type → Type
T R : Type
h : E ~> ExceptT ε (Fitree F)
t : Fitree E T
k : T → Fitree E R
⊢ interpExcept h (bind t k) =
    bind (interpExcept h t) fun x? =>
      match x? with
      | Except.error ε_1 => ret (Except.error ε_1)
      | Except.ok x => interpExcept h (k x)
no goals