IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
compose iter inverses1122 1. A : Type
2. f : AA 3. g : AA 4. InvFuns(A;A;f;g)
5. x : A 6. i : 7. 0<i 8. g{i-1}(f{i-1}(x)) = x g{i-1}(g(f(f{i-1}(x)))) = x
By:
Analyze4 THEN Rewrite by x:A. g(f(x)) = x
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html