IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
fpf-cap-void-subtype A:Type, eq:EqDecider(A), ds:x:A fp-> Type, x:A. ds(x)?Void r ds(x)?Top
By:
Auto THEN Unfold `fpf-cap` 0 THEN SplitOnConclITE THEN Analyze 0
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
A:Type, eq:EqDecider(A), ds:x:A fp-> Type, x:A. ds(x)?Void 
r ds(x)?Top
