rfl
case Ret
E : Type → Type
S : Type
F : Type → Type
R R✝ : Type
k : R → Fitree E R✝
h : E ~> StateT S (Fitree F)
r✝ : R
s : S
⊢ interpState h (bind (Ret r✝) k) s =
    bind (interpState h (Ret r✝) s) fun x =>
      match x with
      | (x, s') => interpState h (k x) s'
no goals