'b,'a:S, x:('a  'b).
  (x:'b. x) o x = x  ('a  'b) & x o (x:'a. x) = x  ('a  'b)

By:	RewriteOfThm Thm* 'b,'a:S. all(f:'a  'b. and(equal(o(i,f),f),equal(o(f,i),f))) (SimpsetC [`hol_to_nuprl`])

None

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