Nuprl - Proof: inv funs iff inv funs 2

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: inv funs iff inv funs 2

A,B:Type, f:(A

B), g:(B

A). InvFuns(A; B; f; g)

InvFuns(A;B;f;g)

By:	Unfolds [`inv_funs_2`;`inv_funs`] 0

Generated subgoal:

1 A,B:Type, f:(AB), g:(BA).
g o f = Id & f o g = Id (x:A. g(f(x)) = x) & (y:B. f(g(y)) = y)
7 steps

About:

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