(27steps total) PrintForm Definitions Lemmas DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: nsub bij ooc invpair 1 3 1 1
1. a : 
2. (f.<f,y.least x:. f(x)=y>)  (a bij a)aa
3. (fg.fg/f,g. f)  (aa)a bij a
4. f : a bij a
  (fg.fg/f,g. f)((f.<f,y.least x:. f(x)=y>)(f)) = f
By: Reduce Concl

Generated subgoals:

None

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

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