---

Step * of Lemma list_accum_pair_wf

∀[T,A,B:Type]. ∀[a0:A]. ∀[b0:B]. ∀[f:A ⟶ T ⟶ A]. ∀[g:B ⟶ T ⟶ B]. ∀[L:T List].
  (list_accum_pair(a,x.f[a;x];b,x.g[b;x];a0;b0;L) ∈ A × B)
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}[T,A,B:Type].  \mforall{}[a0:A].  \mforall{}[b0:B].  \mforall{}[f:A  {}\mrightarrow{}  T  {}\mrightarrow{}  A].  \mforall{}[g:B  {}\mrightarrow{}  T  {}\mrightarrow{}  B].  \mforall{}[L:T  List].
    (list\_accum\_pair(a,x.f[a;x];b,x.g[b;x];a0;b0;L)  \mmember{}  A  \mtimes{}  B)


By

---

Latex:
ProveWfLemma

---

Home Index