Theorem: Fitree.bind_Ret' (MLIR/Semantics/Fitree.lean)

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

State before:
case Ret
E✝ : Type → Type
R✝ : Type
r✝ : R✝
⊢ (bind (Ret r✝) fun r => Ret r) = Ret r✝
Tactic:
rfl
State after:
no goals

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