---

Step * 1 1 of Lemma zip_unzip


1. T1 : Type
2. T2 : Type
3. u : T1 × T2
4. v : (T1 × T2) List
5. zip(map(λp.(fst(p));v);map(λp.(snd(p));v)) = v ∈ ((T1 × T2) List)
⊢ [<fst(u), snd(u)> / zip(map(λp.(fst(p));v);map(λp.(snd(p));v))] = [u / v] ∈ ((T1 × T2) List)
BY
{ (((D (-3) THEN Reduce 0) THEN EqCD) THEN Auto{1,3}-1) }

---

Latex:

---

Latex:

1.  T1  :  Type
2.  T2  :  Type
3.  u  :  T1  \mtimes{}  T2
4.  v  :  (T1  \mtimes{}  T2)  List
5.  zip(map(\mlambda{}p.(fst(p));v);map(\mlambda{}p.(snd(p));v))  =  v
\mvdash{}  [<fst(u),  snd(u)>  /  zip(map(\mlambda{}p.(fst(p));v);map(\mlambda{}p.(snd(p));v))]  =  [u  /  v]


By

---

Latex:
(((D  (-3)  THEN  Reduce  0)  THEN  EqCD)  THEN  Auto\{1,3\}-1)

---

Home Index