IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
compose iter point id121 1. A : Type
2. f : AA 3. u : A 4. f(u) = u 5. i : 6. 0<i 7. f{i-1}(u) = u f(f{i-1}(u)) = u
By:
Rewrite by Hyp:7 ...w
Generated subgoal:
1
f(u) = u
Hypothesis
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
A
i-1}(u) = u
f(f{
