simp [interpState] at *
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},
    interpState h (bind (k✝ a) k) s =
      bind (interpState h (k✝ a) s) fun x =>
        match x with
        | (x, s') => interpState h (k x) s'
⊢ ∀ {s : S},
    interpState h (bind (Vis e✝ k✝) k) s =
      bind (interpState h (Vis e✝ k✝) s) fun x =>
        match x with
        | (x, s') => interpState h (k x) s'
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}, interp h (bind (Vis e✝ k✝) k) s = bind (interp h (Vis e✝ k✝) s) fun x => interp h (k x.fst) x.snd