(5steps total) PrintForm Definitions Lemmas list 1 Sections StandardLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: select wf 1 1 1 1

1. A : Type
2. l : A List
3. n : 
4. 0n
5. n<||l||
  ||l||-n1


By: SupInf'


Generated subgoals:

None

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

(5steps total) PrintForm Definitions Lemmas list 1 Sections StandardLIB Doc