(6steps total) PrintForm Definitions mb event system 1 Sections EventSystems Search Doc
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: select-map
  f:Top, T:Type, L:T List, i:||L||. map(f;L)[i] ~ (f(L[i]))
By: InductionOnList THEN Reduce 0 THEN Analyze 0

Generated subgoals:

1 1. f : Top
2. T : Type
3. T List
4. i : 0
  nil[i] ~ (f(nil[i]))
Auto
2 1. f : Top
2. T : Type
3. T List
4. u : T
5. v : T List
6. i:||v||. map(f;v)[i] ~ (f(v[i]))
7. i : (||v||+1)
  [(f(u)) / map(f;v)][i] ~ (f([u / v][i]))
4 steps

About:
listconsnilnatural_numberapplyuniversesqequaltopall
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html

(6steps total) PrintForm Definitions mb event system 1 Sections EventSystems Search Doc