IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def zip(as;bs)
Def == Case of as Def == Canil nil
Def == Caa.as' Case of bs; nil nil ; b.bs' [<a,b> / zip(as';bs')]
Def (recursive)
is mentioned by
Thm*as:(T1T2) List. zip(1of(unzip(as));2of(unzip(as))) = as