(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
1. a : 
  (a bij a) ~ (aa)
By: Witness:
Wi(f.<f,y.least x:. f(x)=y>)  (a bij a)aa |
Wi(fg.fg/f,g. f)  (aa)a bij a

Generated subgoals:

1   (f.<f,y.least x:. f(x)=y>)  (a bij a)aa
6 steps
2 2. (f.<f,y.least x:. f(x)=y>)  (a bij a)aa
  (fg.fg/f,g. f)  (aa)a bij a
2 steps
3 2. (f.<f,y.least x:. f(x)=y>)  (a bij a)aa
3. (fg.fg/f,g. f)  (aa)a bij a
  InvFuns(a bij a;aa;f.<f,y.least x:. f(x)=y>;fg.fg/f,g. f)
17 steps

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

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