---

Step * of Lemma zip_unzip

∀[T1,T2:Type]. ∀[as:(T1 × T2) List].  (zip(fst(unzip(as));snd(unzip(as))) = as ∈ ((T1 × T2) List))
BY
{ Unfold `unzip` 0 }

1
∀[T1,T2:Type]. ∀[as:(T1 × T2) List].
  (zip(fst(<map(λp.(fst(p));as), map(λp.(snd(p));as)>);snd(<map(λp.(fst(p));as), map(λp.(snd(p));as)>)) = as ∈ ((T1 × T2\000C) List))

---

Latex:

---

Latex:
\mforall{}[T1,T2:Type].  \mforall{}[as:(T1  \mtimes{}  T2)  List].    (zip(fst(unzip(as));snd(unzip(as)))  =  as)


By

---

Latex:
Unfold  `unzip`  0

---

Home Index