IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
fpf-compatible-symmetry A:Type, eq:EqDecider(A), B:(AType), f,g:a:A fp-> B(a). f || gg || f
By:
Auto THEN RepeatFor 3 (ParallelOp -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:(A
Type), f,g:a:A fp-> B(a). f || g 
g || f
