(3steps total) PrintForm Definitions list 1 Sections StandardLIB Search Doc
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: map length
  A,B:Type, f:(AB), as:A List. ||map(f;as)|| = ||as||
By: UnivCD THEN ListInd -1 THEN AbReduce 0

Generated subgoals:

1 1. A : Type
2. B : Type
3. AB
4. A List
  0 = 0
Auto
2 1. A : Type
2. B : Type
3. f : AB
4. A List
5. A
6. v : A List
7. ||map(f;v)|| = ||v||
  ||map(f;v)||+1 = ||v||+1
Auto

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

(3steps total) PrintForm Definitions list 1 Sections StandardLIB Search Doc