---

Step * 1 of Lemma select_zip


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)
BY
{ CaseNat 0 `i'⋅ }

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
11. i = 0 ∈ ℤ
⊢ [<u, u1> / zip(v;v1)][0] = <[u / v][0], [u1 / v1][0]> ∈ (T1 × T2)

2
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
11. ¬(i = 0 ∈ ℤ)
⊢ [<u, u1> / zip(v;v1)][i] = <[u / v][i], [u1 / v1][i]> ∈ (T1 × T2)

---

Latex:

---

Latex:

1.  T1  :  Type
2.  T2  :  Type
3.  u  :  T1
4.  v  :  T1  List
5.  \mforall{}[bs:T2  List].  \mforall{}[i:\mBbbN{}].    zip(v;bs)[i]  =  <v[i],  bs[i]>  supposing  i  <  ||zip(v;bs)||
6.  u1  :  T2
7.  v1  :  T2  List
8.  \mforall{}[i:\mBbbN{}].  zip([u  /  v];v1)[i]  =  <[u  /  v][i],  v1[i]>  supposing  i  <  ||zip([u  /  v];v1)||
9.  i  :  \mBbbN{}
10.  i  <  ||zip(v;v1)||  +  1
\mvdash{}  [<u,  u1>  /  zip(v;v1)][i]  =  <[u  /  v][i],  [u1  /  v1][i]>


By

---

Latex:
CaseNat  0  `i'\mcdot{}

---

Home Index