IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
function wf stype111 1. 'a : {T:Type| x:T. True }
2. 'b : Type
3. 'b 4. True
x:('a'b). True
By:
DTerm (y.x) 0 THEN StrongAuto
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html