---

Step * of Lemma unzip_zip

No Annotations
∀[T1,T2:Type]. ∀[as:T1 List]. ∀[bs:T2 List].
  unzip(zip(as;bs)) = <as, bs> ∈ (T1 List × (T2 List)) supposing ||as|| = ||bs|| ∈ ℤ
BY
{ (Intros THEN RWO "unzip-zip" 0 THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[T1,T2:Type].  \mforall{}[as:T1  List].  \mforall{}[bs:T2  List].    unzip(zip(as;bs))  =  <as,  bs>  supposing  ||as||  =  ||bs||


By

---

Latex:
(Intros  THEN  RWO  "unzip-zip"  0  THEN  Auto)

---

Home Index