---

Step * 1 of Lemma zip_unzip


∀[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))
BY
{ (InductionOnList THEN All Reduce THEN Try (Complete (Auto{1,3}-1))) }

1
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)

---

Latex:

---

Latex:

\mforall{}[T1,T2:Type].  \mforall{}[as:(T1  \mtimes{}  T2)  List].
    (zip(fst(<map(\mlambda{}p.(fst(p));as),  map(\mlambda{}p.(snd(p));as)>);snd(<map(\mlambda{}p.(fst(p));as),  map(\mlambda{}p.(snd(p));as)\000C>))  =  as)


By

---

Latex:
(InductionOnList  THEN  All  Reduce  THEN  Try  (Complete  (Auto\{1,3\}-1)))

---

Home Index