Theorem: Fitree.bind_bind (MLIR/Semantics/Fitree.lean)

State before:
E✝ : Type → Type
R✝² : Type
t : Fitree E✝ R✝²
R✝¹ : Type
k : R✝² → Fitree E✝ R✝¹
R✝ : Type
k' : R✝¹ → Fitree E✝ R✝
⊢ bind (bind t k) k' = bind t fun x => bind (k x) k'
Tactic:
induction t with
| Ret _ => rfl
| Vis _ _ ih => simp [bind, ih]
State after:
no goals

State before:
case Ret
E✝ : Type → Type
R✝² R✝¹ : Type
k : R✝² → Fitree E✝ R✝¹
R✝ : Type
k' : R✝¹ → Fitree E✝ R✝
r✝ : R✝²
⊢ bind (bind (Ret r✝) k) k' = bind (Ret r✝) fun x => bind (k x) k'
Tactic:
rfl
State after:
no goals

State before:
case Vis
E✝ : Type → Type
R✝² R✝¹ : Type
k : R✝² → Fitree E✝ R✝¹
R✝ : Type
k' : R✝¹ → Fitree E✝ R✝
T✝ : Type
e✝ : E✝ T✝
k✝ : T✝ → Fitree E✝ R✝²
ih : ∀ (a : T✝), bind (bind (k✝ a) k) k' = bind (k✝ a) fun x => bind (k x) k'
⊢ bind (bind (Vis e✝ k✝) k) k' = bind (Vis e✝ k✝) fun x => bind (k x) k'
Tactic:
simp [bind, ih]
State after:
no goals