---

Step * 2 2 of Lemma member-zip


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)})
6. u1 : B@i
7. v1 : B List@i
8. ∀x:A. ∀y:B.  ((<x, y> ∈ zip([u / v];v1)) ⇒ {(x ∈ [u / v]) ∧ (y ∈ v1)})
⊢ ∀x:A. ∀y:B.  ((<x, y> ∈ zip([u / v];[u1 / v1])) ⇒ {(x ∈ [u / v]) ∧ (y ∈ [u1 / v1])})
BY
{ TACTIC:(((Reduce 0 THEN Auto THEN (RWO "cons_member" (-1))) THENA Auto) THEN (D (-1))) }

1
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)})
6. u1 : B@i
7. v1 : B List@i
8. ∀x:A. ∀y:B.  ((<x, y> ∈ zip([u / v];v1)) ⇒ {(x ∈ [u / v]) ∧ (y ∈ v1)})
9. x : A@i
10. y : B@i
11. <x, y> = <u, u1> ∈ (A × B)
⊢ {(x ∈ [u / v]) ∧ (y ∈ [u1 / v1])}

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)})
6. u1 : B@i
7. v1 : B List@i
8. ∀x:A. ∀y:B.  ((<x, y> ∈ zip([u / v];v1)) ⇒ {(x ∈ [u / v]) ∧ (y ∈ v1)})
9. x : A@i
10. y : B@i
11. (<x, y> ∈ zip(v;v1))
⊢ {(x ∈ [u / v]) ∧ (y ∈ [u1 / v1])}

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  [B]  :  Type
3.  u  :  A@i
4.  v  :  A  List@i
5.  \mforall{}ys:B  List.  \mforall{}x:A.  \mforall{}y:B.    ((<x,  y>  \mmember{}  zip(v;ys))  {}\mRightarrow{}  \{(x  \mmember{}  v)  \mwedge{}  (y  \mmember{}  ys)\})
6.  u1  :  B@i
7.  v1  :  B  List@i
8.  \mforall{}x:A.  \mforall{}y:B.    ((<x,  y>  \mmember{}  zip([u  /  v];v1))  {}\mRightarrow{}  \{(x  \mmember{}  [u  /  v])  \mwedge{}  (y  \mmember{}  v1)\})
\mvdash{}  \mforall{}x:A.  \mforall{}y:B.    ((<x,  y>  \mmember{}  zip([u  /  v];[u1  /  v1]))  {}\mRightarrow{}  \{(x  \mmember{}  [u  /  v])  \mwedge{}  (y  \mmember{}  [u1  /  v1])\})


By

---

Latex:
TACTIC:(((Reduce  0  THEN  Auto  THEN  (RWO  "cons\_member"  (-1)))  THENA  Auto)  THEN  (D  (-1)))

---

Home Index