T:Type, f:(TT), m:(T).
  (x:T. m(f(x))m(x) & (m(f(x)) = m(x)  f(x) = x))
  
  (x:T. n:. f(f^n(x)) = f^n(x))

1

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   n:. f(f^n(x)) = f^n(x)

27 steps

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