(6steps total) PrintForm Definitions list 1 Sections StandardLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: length tl 1 1
1. A : Type
2. A List
  ||nil||1  ||tl(nil)|| = ||nil||-1
By: (Analyze 0) THEN (AbReduce -1)

Generated subgoal:

1 3. 01
  ||tl(nil)|| = ||nil||-1
1 step

About:
listnilintnatural_numbersubtractuniverseequalimplies
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

(6steps total) PrintForm Definitions list 1 Sections StandardLIB Doc