Nuprl - Proof: iter perm cycles uniform2 1 1

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

1. k :

2. f :

k
3. Inj(

k; f) [not for witness]
4.

k. f{

i}(u) = u

. f{

i} = Id

By:	SimilarTo: Hyp:-1 ...

Generated subgoal:

1 3. Inj(k; k; f)
4. i :
5. u:k. f{i}(u) = u
f{i} = Id
1 step

About:

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