Thm*  InvFuns(A;B;f;g)  Inj(A; B; f)

To show Inj(A; B; f) is just to show that

f(a1) = f(a2)  a1 = a2, which is so since

f(a1) = f(a2)  g(f(a1)) = g(f(a2)), and g cancels f, i.e., x:A. g(f(x)) = x, by assumption,

so, a1 = a2.

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html