---

Step * of Lemma list_accum2_wf

∀[A,B,T:Type].
  ∀[f:T ⟶ A ⟶ B ⟶ T]. ∀[g:T ⟶ A ⟶ T]. ∀[h:T ⟶ B ⟶ T]. ∀[as:A List]. ∀[bs:B List]. ∀[y:T].
    (list_accum2(x,a,b.f[x;a;b];x,a.g[x;a];x,b.h[x;b];y;as;bs) ∈ T) 
  supposing value-type(T)
BY
{ (RepeatFor 2 (InductionOnList)
   THEN RecUnfold `list_accum2` 0
   THEN Reduce 0
   THEN Auto
   THEN RepUR ``nil it`` -2
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A,B,T:Type].
    \mforall{}[f:T  {}\mrightarrow{}  A  {}\mrightarrow{}  B  {}\mrightarrow{}  T].  \mforall{}[g:T  {}\mrightarrow{}  A  {}\mrightarrow{}  T].  \mforall{}[h:T  {}\mrightarrow{}  B  {}\mrightarrow{}  T].  \mforall{}[as:A  List].  \mforall{}[bs:B  List].  \mforall{}[y:T].
        (list\_accum2(x,a,b.f[x;a;b];x,a.g[x;a];x,b.h[x;b];y;as;bs)  \mmember{}  T) 
    supposing  value-type(T)


By

---

Latex:
(RepeatFor  2  (InductionOnList)
  THEN  RecUnfold  `list\_accum2`  0
  THEN  Reduce  0
  THEN  Auto
  THEN  RepUR  ``nil  it``  -2
  THEN  Auto)

---

Home Index