IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
ma-state-subtype2 ds,ds':ltg:Id fp-> Type. dsds' State(ds') State(ds)
By:
Auto THEN Analyze 0 THEN DoSubsume
THEN
BackThru Thm*ds,ds':ltg:Id fp-> Type. dsds' (State(ds') r State(ds))
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
ds,ds':ltg:Id fp-> Type. ds 
ds' 
State(ds') 
