(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:ki:f{i}(u) = u
  i:u:kf{i}(u) = u


By: Analyze2


Generated subgoal:

1 2. f : kk
3. Inj(kkf)
4. u:ki:f{i}(u) = u
  i:u:kf{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