---

Step * of Lemma unzip-un-zip

∀[as:(Top × Top) List]. (unzip(as) ~ un-zip(as))
BY
{ xxx(Unfolds ``unzip un-zip`` 0
      THEN InductionOnList
      THEN Reduce 0
      THEN Try (Trivial)
      THEN DVar `u'
      THEN Reduce 0
      THEN RevHypSubst (-1) 0
      THEN Reduce 0
      THEN Auto)xxx }

---

Latex:

---

Latex:
\mforall{}[as:(Top  \mtimes{}  Top)  List].  (unzip(as)  \msim{}  un-zip(as))


By

---

Latex:
xxx(Unfolds  ``unzip  un-zip``  0
        THEN  InductionOnList
        THEN  Reduce  0
        THEN  Try  (Trivial)
        THEN  DVar  `u'
        THEN  Reduce  0
        THEN  RevHypSubst  (-1)  0
        THEN  Reduce  0
        THEN  Auto)xxx

---

Home Index