1. a : 
2. f : a bij a
3. f  a onto a
4. f  aa
5. Bij(a; a; f)  [not for witness]
  InvFuns(a;a;f;y.least x:. f(x)=y)

By:	Use:[a | a | f] Inst: Thm*  f:(a onto b). (y.least x:. f(x)=y)  b inj a THEN Analyze-1

1

6. (y.least x:. f(x)=y)  aa 7. Inj(a; a; y.least x:. f(x)=y)  [not for witness]   InvFuns(a;a;f;y.least x:. f(x)=y)

6 steps

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