1. T : Type
2. f : TT
3. m : T
4. x:T. m(f(x))m(x) & (m(f(x)) = m(x)  f(x) = x)
5. x : T
6. n : 
7. 0<n
8. m(f^n-1(x))m(x)-(n-1)  f(f^n-1(x)) = f^n-1(x)
  m(f^n(x))m(x)-n  f(f^n(x)) = f^n(x)

1	8. m(f^n-1(x))m(x)-(n-1)   m(f^n(x))m(x)-n  f(f^n(x)) = f^n(x)	7 steps
2	8. f(f^n-1(x)) = f^n-1(x)   m(f^n(x))m(x)-n  f(f^n(x)) = f^n(x)	5 steps

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