---

Step * of Lemma list-accum_wf

∀[T,T':Type]. ∀[l:T List]. ∀[b:T']. ∀[f:(T List) ⟶ T' ⟶ T ⟶ T'].  (list-accum(t,a,h.f[t;a;h];b;l) ∈ T')
BY
{ (InductionOnList THEN Unfold `list-accum` 0 THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T,T':Type].  \mforall{}[l:T  List].  \mforall{}[b:T'].  \mforall{}[f:(T  List)  {}\mrightarrow{}  T'  {}\mrightarrow{}  T  {}\mrightarrow{}  T'].
    (list-accum(t,a,h.f[t;a;h];b;l)  \mmember{}  T')


By

---

Latex:
(InductionOnList  THEN  Unfold  `list-accum`  0  THEN  Reduce  0  THEN  Auto)

---

Home Index