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