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