induction t with
| Ret _ => rfl
| Vis _ _ ih =>
    simp [interpOption] at *
    simp [interp, bind, Bind.bind, OptionT.bind, OptionT.mk]
    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 F : Type → Type
T R : Type
h : E ~> OptionT (Fitree F)
t : Fitree E T
k : T → Fitree E R
⊢ interpOption h (bind t k) =
    bind (interpOption h t) fun x? =>
      match x? with
      | some x => interpOption h (k x)
      | none => ret none
no goals