IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
fpf-single-sub-reflexive A:Type, B:(AType), x:A, v:B(x), eqa:EqDecider(A). x : vx : v
By:
Auto
THEN
BackThru Thm*B:(AType), eq:EqDecider(A), f,g:a:A fp-> B(a). f = gfg
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
A:Type, B:(A
Type), x:A, v:B(x), eqa:EqDecider(A). x : v 
x : v
f 
