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` THEN Reduce 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