Nuprl - Proof: iter perm cycles uniform2 1

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

1. k :

2. f :

k inj

k
3.

k. f{

i}(u) = u

. f{

i} = Id

By:

Analyze-2

Generated subgoal:

1 2. f : kk
3. Inj(k; k; f) [not for witness]
4. i:. u:k. f{i}(u) = u
i:. f{i} = Id
2 steps

About:

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