---

Step * of Lemma select_zip

∀[T1,T2:Type]. ∀[as:T1 List]. ∀[bs:T2 List]. ∀[i:ℕ].
  zip(as;bs)[i] = <as[i], bs[i]> ∈ (T1 × T2) supposing i < ||zip(as;bs)||
BY
{ (InductionOnList THEN Try (InductionOnList⋅) THEN RecUnfold `zip` 0 THEN Reduce 0 THEN Auto) }

1
1. T1 : Type
2. T2 : Type
3. u : T1
4. v : T1 List
5. ∀[bs:T2 List]. ∀[i:ℕ].  zip(v;bs)[i] = <v[i], bs[i]> ∈ (T1 × T2) supposing i < ||zip(v;bs)||
6. u1 : T2
7. v1 : T2 List
8. ∀[i:ℕ]. zip([u / v];v1)[i] = <[u / v][i], v1[i]> ∈ (T1 × T2) supposing i < ||zip([u / v];v1)||
9. i : ℕ
10. i < ||zip(v;v1)|| + 1
⊢ [<u, u1> / zip(v;v1)][i] = <[u / v][i], [u1 / v1][i]> ∈ (T1 × T2)

---

Latex:

---

Latex:
\mforall{}[T1,T2:Type].  \mforall{}[as:T1  List].  \mforall{}[bs:T2  List].  \mforall{}[i:\mBbbN{}].
    zip(as;bs)[i]  =  <as[i],  bs[i]>  supposing  i  <  ||zip(as;bs)||


By

---

Latex:
(InductionOnList  THEN  Try  (InductionOnList\mcdot{})  THEN  RecUnfold  `zip`  0  THEN  Reduce  0  THEN  Auto)

---

Home Index