IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
nil before T:Type, x,y:T. x before y nil False
By:
((Unfold `l_before` 0) THEN (RWO Thm*x:T, L:T List. [x / L] nil False 0))
THEN
SimpConcl
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,y:T. x before y 
nil 
False
nil 
