Theorem: Fitree.interp'_bind (MLIR/Semantics/Fitree.lean)

State before:
E✝ : Type → Type
h : E✝ ~> Fitree Void1
F✝ : Type → Type
R✝¹ : Type
t : Fitree (E✝ +' F✝) R✝¹
R✝ : Type
k : R✝¹ → Fitree (E✝ +' F✝) R✝
⊢ interp' h (bind t k) = bind (interp' h t) fun x => interp' h (k x)
Tactic:
simp [interp', interp_bind]
State after:
no goals