Theorem: Fitree.bind_assoc (MLIR/Semantics/FitreeLaws.lean)

State before:
E : Type → Type
R₁ R₂ R₃ : Type
t : Fitree E R₁
k₁ : R₁ → Fitree E R₂
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];
State after:
no goals

State before:
case Ret
E : Type → Type
R₁ R₂ R₃ : Type
k₁ : R₁ → Fitree E R₂
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₂ R₃ : Type
k₁ : R₁ → Fitree E R₂
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]
State after:
no goals