IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
fpf-cap wf A:Type, B:(AType), f:a:A fp-> B(a), eq:EqDecider(A), x:A, z:B(x).
f(x)?zB(x)
By:
Auto THEN Unfold `fpf-cap` 0 THEN SplitOnConclITE THEN FpfSubtype
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
A:Type, B:(A
Type), f:a:A fp-> B(a), eq:EqDecider(A), x:A, z:B(x).
f(x)?z 
B(x)
