induction t with
| Ret _ => intros s; rfl
| Vis _ _ ih =>
  simp [interpState] at *
  simp [interp, Bind.bind, StateT.bind]
  simp [ih]
E : Type → Type
S : Type
F : Type → Type
R R✝ : Type
k : R → Fitree E R✝
h : E ~> StateT S (Fitree F)
t : Fitree E R
⊢ ∀ {s : S},
    interpState h (bind t k) s =
      bind (interpState h t s) fun x =>
        match x with
        | (x, s') => interpState h (k x) s'
no goals