IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
card nsub0 union
A:Type. (
0+A) ~ A
Generated subgoal:
| 1 |
1. A : Type
( 0+A) ~ A
 | 5 steps |
About:
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html