IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
sfa doc sexpr fp2 1. A : Type
2. X : (Sexpr(A)Sexpr(A))+A X Sexpr(A)
By:
Analyze
Generated subgoal:
1
X (Sexpr(A)Sexpr(A))+A
Trivial
About:
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html