simp [bind]
case Vis
E : Type → Type
R₁ R₂ R₃ : Type
k₁ : R₁ → Fitree E R₂
k₂ : R₂ → Fitree E R₃
T✝ : Type
e✝ : E T✝
k✝ : T✝ → Fitree E R₁
ih : ∀ (a : T✝), bind (bind (k✝ a) k₁) k₂ = bind (k✝ a) fun x => bind (k₁ x) k₂
⊢ bind (bind (Vis e✝ k✝) k₁) k₂ = bind (Vis e✝ k✝) fun x => bind (k₁ x) k₂
no goals