IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
not nil cons2
1
1. 'a : S
2. t : 'a List
3. h : 'a
nil = cons(h; t) 
False
Generated subgoals:
1 |
nil = cons(h; t)  False
 | 3 steps |
2 |
(nil = cons(h; t))  False
 | Auto |
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html