IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
compose iter inverses111 1. A : Type
2. f : AA 3. g : AA 4. InvFuns(A;A;f;g)
5. x : A g{0}(f{0}(x)) = x
By:
Compute g{0}(f{0}(x)) *x
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
A
g{
0}(f{
x
