induction t with
| Ret _ => rfl
| Vis _ _ ih => simp [bind, ih]
E✝¹ E✝ : Type → Type
h : E✝¹ ~> Fitree E✝
R✝¹ : Type
t : Fitree E✝¹ R✝¹
R✝ : Type
k : R✝¹ → Fitree E✝¹ R✝
⊢ interp h (bind t k) = bind (interp h t) fun x => interp h (k x)
no goals