IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
fpf-trivial-subtype-top A:Type, B:(AType), f:a:A fp-> B(a). fa:A fp-> Top
By:
Auto THEN FpfSubtype
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, B:(A
Type), f:a:A fp-> B(a). f 
a:A fp-> Top
