---

Step * of Lemma run-to-n_wf

∀[B1,a1:Type]. ∀[r:ℤ ⟶ (a1 × B1)]. ∀[n:ℤ].  (run-to-n(r;n) ∈ a1 List)
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}[B1,a1:Type].  \mforall{}[r:\mBbbZ{}  {}\mrightarrow{}  (a1  \mtimes{}  B1)].  \mforall{}[n:\mBbbZ{}].    (run-to-n(r;n)  \mmember{}  a1  List)


By

---

Latex:
ProveWfLemma

---

Home Index