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
  InvFuns(a bij a;aa;f.<f,y.least x:. f(x)=y>;fg.fg/f,g. f)

1	x:(a bij a). (fg.fg/f,g. f)((f.<f,y.least x:. f(x)=y>)(x)) = x	2 steps
2	y:(aa). (f.<f,y.least x:. f(x)=y>)((fg.fg/f,g. f)(y)) = y	14 steps

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