IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
fpf-cap-wf-univ A:Type, f:a:A fp-> Type, eq:EqDecider(A), x:A, z:Type. f(x)?z Type
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, f:a:A fp-> Type, eq:EqDecider(A), x:A, z:Type. f(x)?z 
Type
