IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
cons sublist nil T:Type, x:T, L:T List. [x / L] nil False
By:
Auto THEN FwdThru Thm*L1,L2:T List. L1L2 ||L1||||L2|| [-1]
THEN
Reduce -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, x:T, L:T List. [x / L] 
nil 
False
||L2|| [-1]
