---

Step * 1 of Lemma member-zip


1. [A] : Type
2. [B] : Type
⊢ ∀ys:B List. ∀x:A. ∀y:B.  ((<x, y> ∈ zip([];ys)) ⇒ {(x ∈ []) ∧ (y ∈ ys)})
BY
{ TACTIC:(Reduce 0 THEN Auto THEN (ObviousFrom [(-1)])) }

---

Latex:

---

Latex:

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


By

---

Latex:
TACTIC:(Reduce  0  THEN  Auto  THEN  (ObviousFrom  [(-1)]))

---

Home Index