---

Step * of Lemma cps-accum_wf

∀[A,B,C:Type]. ∀[f:(B ⟶ C) ⟶ A ⟶ B ⟶ C]. ∀[b:B]. ∀[L:A List].  (cps-accum(k,a.f[k;a];b;L) ∈ (B ⟶ C) ⟶ C)
BY
{ (InductionOnList THEN Unfold `cps-accum` 0 THEN Reduce 0 THEN Try (Fold `cps-accum` 0⋅) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A,B,C:Type].  \mforall{}[f:(B  {}\mrightarrow{}  C)  {}\mrightarrow{}  A  {}\mrightarrow{}  B  {}\mrightarrow{}  C].  \mforall{}[b:B].  \mforall{}[L:A  List].
    (cps-accum(k,a.f[k;a];b;L)  \mmember{}  (B  {}\mrightarrow{}  C)  {}\mrightarrow{}  C)


By

---

Latex:
(InductionOnList  THEN  Unfold  `cps-accum`  0  THEN  Reduce  0  THEN  Try  (Fold  `cps-accum`  0\mcdot{})  THEN  Auto)

---

Home Index