IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
zip wf T1,T2:Type, as:T1 List, bs:T2 List. zip(as;bs) (T1T2) List
By:
((Analyze 0) THEN (Analyze 0) THEN (Analyze 0)) THEN ListInd -1
THEN
RecUnfold `zip` 0
THEN
Reduce 0
THEN
Try (Complete Auto)
THEN
Analyze 0
THEN
ListInd -1
THEN
Reduce 0
1. T1 : Type
2. T2 : Type
3. T1 List
4. u : T1 5. v : T1 List
6. bs:T2 List. zip(v;bs) (T1T2) List
7. T2 List
8. T2 9. v1 : T2 List
10. (Case of v1; nil nil ; b.bs' [<u,b> / zip(v;bs')]) (T1T2) List
zip(v;v1) (T1T2) List
1 step
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html