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:
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
T:Type, L:T List. 
L = nil 
0<||L||
