Nuprl - Proof: iter perm cycles uniform 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: iter perm cycles uniform 1 1

1. k :

2. f :

k
3. Inj(

k; f)
4.

. f{

i}(u) = u

k. f{

i}(u) = u

By:	FwdThru: Thm* k:, Q:(kAProp). Thm* (x:k. y:A. Q(x;y)) (f:(kA). x:k. Q(x;f(x))) on [ Hyp:-1 ] THEN New:h Analyze-1

Generated subgoal:

1 5. h : k
6. u:k. f{h(u)}(u) = u
i:. u:k. f{i}(u) = u
11 steps

About:

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