simp [bind, ih]
case Vis
E✝ : Type → Type
R✝² R✝¹ : Type
k : R✝² → Fitree E✝ R✝¹
R✝ : Type
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