(3steps total) PrintForm Definitions mb list 1 Sections MarkB generic Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: zip unzip
  T1,T2:Type, as:(T1T2) List. zip(1of(unzip(as));2of(unzip(as))) = as
By: Unfold `unzip` 0

Generated subgoal:

1   T1,T2:Type, as:(T1T2) List.
  zip(1of(<map(p.1of(p);as),map(p.2of(p);as)>);2of(<map(p.1of(p);as)
  zip(1of(<map(p.1of(p);as),map(p.2of(p);as)>);2of(,map(p.2of(p);as)>))
  =
  as
2 steps

About:
pairproductlistlambdauniverseequalall
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

(3steps total) PrintForm Definitions mb list 1 Sections MarkB generic Doc