IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
iter perm cycles uniform2111 1. k : 2. f : kk 3. Inj(k; k; f)
4. i : 5. u:k. f{i}(u) = u f{i} = Id
By:
FunExtensionality THEN BackThru: Hyp:5 ...w
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
u:
i}(u) = u
f{
