---

Step * 1 of Lemma zip_length


1. T1 : Type
2. T2 : Type
⊢ ∀[bs:T2 List]. ((||zip([];bs)|| ≤ ||[]||) ∧ (||zip([];bs)|| ≤ ||bs||))
BY
{ (RecUnfold `zip` 0 THEN Reduce 0 THEN Auto') }

---

Latex:

---

Latex:

1.  T1  :  Type
2.  T2  :  Type
\mvdash{}  \mforall{}[bs:T2  List].  ((||zip([];bs)||  \mleq{}  ||[]||)  \mwedge{}  (||zip([];bs)||  \mleq{}  ||bs||))


By

---

Latex:
(RecUnfold  `zip`  0  THEN  Reduce  0  THEN  Auto')

---

Home Index