IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
fpf-sub transitivity A:Type, B:(AType), eq:EqDecider(A), f,g,h:a:A fp-> B(a).
fgghfh
By:
Auto THEN All (Unfold `fpf-sub`) THEN ParallelOp -2 THEN ParallelOp -1
THEN
InstHyp [x] -4
THEN
ExRepD
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
A:Type, B:(A
Type), eq:EqDecider(A), f,g,h:a:A fp-> B(a).
f 
g 
g 
