simp [ih]
case Vis
E : Type → Type
S : Type
F : Type → Type
R R✝ : Type
k : R → Fitree E R✝
h : E ~> StateT S (Fitree F)
T✝ : Type
e✝ : E T✝
k✝ : T✝ → Fitree E R
ih : ∀ (a : T✝) {s : S}, interp h (bind (k✝ a) k) s = bind (interp h (k✝ a) s) fun x => interp h (k x.fst) x.snd
⊢ ∀ {s : S},
    (bind (h T✝ e✝ s) fun __discr => interp h (bind (k✝ __discr.fst) k) __discr.snd) =
      bind (h T✝ e✝ s) fun x => bind (interp h (k✝ x.fst) x.snd) fun x => interp h (k x.fst) x.snd
no goals