apply Fitree.interpState_bind
α σ : Type
ε : σ → Type
E : Type → Type
T R : Type
δ : Dialect α σ ε
t : Fitree (SSAEnvE δ +' E) T
k : T → Fitree (SSAEnvE δ +' E) R
s₁ : SSAEnv δ
⊢ interpSSA' (Fitree.bind t k) s₁ =
    Fitree.bind (interpSSA' t s₁) fun x =>
      match x with
      | (x, s₂) => interpSSA' (k x) s₂
no goals