IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
fpf-empty-compatible-right A:Type, eq:EqDecider(A), B:Top, f:a:A fp-> Top. f ||
By:
Auto THEN Unfolds [`fpf-compatible`] 0 THEN Unfolds [`fpf-dom`;`fpf-empty`] -1
THEN
Reduce -1
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
A:Type, eq:EqDecider(A), B:Top, f:a:A fp-> Top. f || 
