IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
fpf-empty-compatible-left 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`] -2
THEN
Reduce -2
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
