---

Step * of Lemma mklist-general_wf

∀[T3:Type]. ∀[n:ℕ]. ∀[h:(T3 List) ⟶ T3].  (mklist-general(n;h) ∈ T3 List)
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}[T3:Type].  \mforall{}[n:\mBbbN{}].  \mforall{}[h:(T3  List)  {}\mrightarrow{}  T3].    (mklist-general(n;h)  \mmember{}  T3  List)


By

---

Latex:
ProveWfLemma

---

Home Index