English
The evaluation of the sequential composition (k.then k') on input v equals the bind of k.eval v with k'.eval.
Русский
Оценка последовательного применения (k.then k') на v равна связыванию (bind) k.eval v и k'.eval.
LaTeX
$$$(k.then k').eval(v) = k.eval(v) \\bind k'.eval$$$
Lean4
theorem then_eval {k k' : Cont} {v} : (k.then k').eval v = k.eval v >>= k'.eval := by
induction k generalizing v with
| halt => simp only [Cont.eval, Cont.then, pure_bind]
| cons₁ => simp only [Cont.eval, Cont.then, bind_assoc, *]
| cons₂ => simp only [Cont.eval, Cont.then, *]
| comp _ _ k_ih => simp only [Cont.eval, Cont.then, bind_assoc, ← k_ih]
| fix _ _ k_ih =>
simp only [Cont.eval, Cont.then, *]
split_ifs <;> [rfl; simp only [← k_ih, bind_assoc]]
