IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
There is an older definition of inverse functions
Def InvFuns(A; B; f; g) == g o f = Id & f o g = Id
and we use
Thm* InvFuns(A; B; f; g) 
InvFuns(A;B;f;g)
to mediate bewteen them.
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
