PrintForm Definitions mb list 1 Sections MarkB generic Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: non nil length
  T:Type, L:T List. L = nil  0<||L||
By: Auto THEN ListInd -2 THEN Reduce 0 THEN Analyze -1

Generated subgoals:

None

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

PrintForm Definitions mb list 1 Sections MarkB generic Doc