---

Step * of Lemma select-zip

∀[as,bs:Top List]. ∀[i:ℕ].  zip(as;bs)[i] ~ <as[i], bs[i]> supposing i < ||as|| ∧ i < ||bs||
BY
{ ((RepeatFor 2 ((InductionOnList THENA Auto)) THEN Reduce 0)
   THEN Auto
   THEN CaseNat 0 `i'⋅
   THEN Reduce 0
   THEN Try (Trivial)
   THEN ((RWO "select-cons" 0 THENA Auto) THEN AutoSplit)
   THEN RWO "4" 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[as,bs:Top  List].  \mforall{}[i:\mBbbN{}].    zip(as;bs)[i]  \msim{}  <as[i],  bs[i]>  supposing  i  <  ||as||  \mwedge{}  i  <  ||bs||


By

---

Latex:
((RepeatFor  2  ((InductionOnList  THENA  Auto))  THEN  Reduce  0)
  THEN  Auto
  THEN  CaseNat  0  `i'\mcdot{}
  THEN  Reduce  0
  THEN  Try  (Trivial)
  THEN  ((RWO  "select-cons"  0  THENA  Auto)  THEN  AutoSplit)
  THEN  RWO  "4"  0
  THEN  Auto)

---

Home Index