---

Step * of Lemma unzip_wf

∀[T1,T2:Type]. ∀[as:(T1 × T2) List].  (unzip(as) ∈ T1 List × (T2 List))
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}[T1,T2:Type].  \mforall{}[as:(T1  \mtimes{}  T2)  List].    (unzip(as)  \mmember{}  T1  List  \mtimes{}  (T2  List))


By

---

Latex:
ProveWfLemma

---

Home Index