simp [interp', interp_bind]
E✝ : Type → Type
h : E✝ ~> Fitree Void1
F✝ : Type → Type
R✝¹ : Type
t : Fitree (E✝ +' F✝) R✝¹
R✝ : Type
k : R✝¹ → Fitree (E✝ +' F✝) R✝
⊢ interp' h (bind t k) = bind (interp' h t) fun x => interp' h (k x)
no goals