(14steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: iter perm cycles uniform 1

1. k : 
2. f : k inj k
3. u:k. i:. f{i}(u) = u
  i:. u:k. f{i}(u) = u


By: Analyze2


Generated subgoal:

1 2. f : kk
3. Inj(k; k; f)
4. u:k. i:. f{i}(u) = u
  i:. u:k. f{i}(u) = u

12 steps

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

(14steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc