(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 length
  T1,T2:Type, as:T1 List, bs:T2 List.
  ||zip(as;bs)||||as|| & ||zip(as;bs)||||bs||
By: ((Analyze 0) THEN (Analyze 0) THEN (Analyze 0)) THEN ListInd -1 THEN Analyze 0
THEN
ListInd -1
THEN
RecUnfold `zip` 0
THEN
Reduce 0
THEN
Try (Complete Auto)

Generated subgoals:

1 1. T1 : Type
2. T2 : Type
3. T1 List
4. T2 List
5. T2
6. v : T2 List
7. ||zip(nil;v)||||nil|| & ||zip(nil;v)||||v||
  00 & 0||v||+1
1 step
2 1. T1 : Type
2. T2 : Type
3. T1 List
4. u : T1
5. v : T1 List
6. bs:T2 List. ||zip(v;bs)||||v|| & ||zip(v;bs)||||bs||
7. T2 List
8. T2
9. v1 : T2 List
10. ||zip([u / v];v1)||||[u / v]|| & ||zip([u / v];v1)||||v1||
  ||zip(v;v1)||+1||v||+1 & ||zip(v;v1)||+1||v1||+1
1 step

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