---

Step * of Lemma zip_wf

∀[T1,T2:Type]. ∀[as:T1 List]. ∀[bs:T2 List].  (zip(as;bs) ∈ (T1 × T2) List)
BY
{ TACTIC:TACTIC:(InductionOnList THEN Auto THEN Try (ListInd (-1)) THEN RecUnfold `zip` 0 THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T1,T2:Type].  \mforall{}[as:T1  List].  \mforall{}[bs:T2  List].    (zip(as;bs)  \mmember{}  (T1  \mtimes{}  T2)  List)


By

---

Latex:
TACTIC:TACTIC:(InductionOnList
                              THEN  Auto
                              THEN  Try  (ListInd  (-1))
                              THEN  RecUnfold  `zip`  0
                              THEN  Reduce  0
                              THEN  Auto)

---

Home Index