IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
sfa doc void dom fun degenerate2 1. A : Type
2. X : {x.x:VoidA}
X VoidA
By:
Analyze-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
x.x:Void
A}
X 
Void
