---

Step * of Lemma member-zip

∀[A,B:Type].  ∀xs:A List. ∀ys:B List. ∀x:A. ∀y:B.  ((<x, y> ∈ zip(xs;ys)) ⇒ {(x ∈ xs) ∧ (y ∈ ys)})
BY
{ InductionOnList }

1
1. [A] : Type
2. [B] : Type
⊢ ∀ys:B List. ∀x:A. ∀y:B.  ((<x, y> ∈ zip([];ys)) ⇒ {(x ∈ []) ∧ (y ∈ ys)})

2
1. [A] : Type
2. [B] : Type
3. u : A@i
4. v : A List@i
5. ∀ys:B List. ∀x:A. ∀y:B.  ((<x, y> ∈ zip(v;ys)) ⇒ {(x ∈ v) ∧ (y ∈ ys)})@i
⊢ ∀ys:B List. ∀x:A. ∀y:B.  ((<x, y> ∈ zip([u / v];ys)) ⇒ {(x ∈ [u / v]) ∧ (y ∈ ys)})

---

Latex:

---

Latex:
\mforall{}[A,B:Type].    \mforall{}xs:A  List.  \mforall{}ys:B  List.  \mforall{}x:A.  \mforall{}y:B.    ((<x,  y>  \mmember{}  zip(xs;ys))  {}\mRightarrow{}  \{(x  \mmember{}  xs)  \mwedge{}  (y  \mmember{}  ys)\})


By

---

Latex:
InductionOnList

---

Home Index