PrintForm Definitions mb list 1 Sections MarkB generic Search Doc
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/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 http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html

PrintForm Definitions mb list 1 Sections MarkB generic Search Doc