---

Step * of Lemma index-split_wf

∀[T:Type]. ∀[L:T List]. ∀[ids:ℕ List].  (index-split(L;ids) ∈ T List × (T List))
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[L:T  List].  \mforall{}[ids:\mBbbN{}  List].    (index-split(L;ids)  \mmember{}  T  List  \mtimes{}  (T  List))


By

---

Latex:
ProveWfLemma

---

Home Index