(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 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
By: InductionOnList THEN All Reduce THEN Try (Complete Auto)

Generated subgoal:

1 1. T1 : Type
2. T2 : Type
3. (T1T2) List
4. u : T1T2
5. v : (T1T2) List
6. zip(map(p.1of(p);v);map(p.2of(p);v)) = v
  [<1of(u),2of(u)> / zip(map(p.1of(p);v);map(p.2of(p);v))] = [u / v]
1 step

About:
pairproductlistconslambdauniverseequalall
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