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)
9. m(f^n(x))m(f^n-1(x))
10. m(f^n(x)) = m(f^n-1(x))  f^n(x) = f^n-1(x)
11. m(f^n(x))<m(f^n-1(x))
  m(f^n(x))m(x)-n  f(f^n(x)) = f^n(x)

1

10. m(f^n(x))<m(f^n-1(x)) 11. f^n(x) = f^n-1(x)   f(f^n(x)) = f^n(x)

2 steps

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