induction t with
| Ret _ => rfl
| Vis _ _ ih => simp [bind];
E : Type → Type
R₁ R₂ R₃ : Type
t : Fitree E R₁
k₁ : R₁ → Fitree E R₂
k₂ : R₂ → Fitree E R₃
⊢ bind (bind t k₁) k₂ = bind t fun x => bind (k₁ x) k₂
no goals