'b,'a:S.
  all
  (P:'a  hbool. all
  (P:'a  hbool. (rep:'b  'a. equal
  (P:'a  hbool. (rep:'b  'a. (type_definition(P,rep)
  (P:'a  hbool. (rep:'b  'a. ,and
  (P:'a  hbool. (rep:'b  'a. ,(all
  (P:'a  hbool. (rep:'b  'a. ,((x':'b. all
  (P:'a  hbool. (rep:'b  'a. ,((x':'b. (x'':'b. implies
  (P:'a  hbool. (rep:'b  'a. ,((x':'b. (x'':'b. (equal
  (P:'a  hbool. (rep:'b  'a. ,((x':'b. (x'':'b. ((rep(x')
  (P:'a  hbool. (rep:'b  'a. ,((x':'b. (x'':'b. (,rep(x''))
  (P:'a  hbool. (rep:'b  'a. ,((x':'b. (x'':'b. ,equal(x',x''))))
  (P:'a  hbool. (rep:'b  'a. ,,all
  (P:'a  hbool. (rep:'b  'a. ,,(x:'a. equal
  (P:'a  hbool. (rep:'b  'a. ,,(x:'a. (P(x)
  (P:'a  hbool. (rep:'b  'a. ,,(x:'a. ,exists
  (P:'a  hbool. (rep:'b  'a. ,,(x:'a. ,(x':'b. equal(x,rep(x')))))))))

1

1. 'b : S 2. 'a : S 3. P : 'a 4. rep : 'b'a   (type_definition('a;'b;P;rep))   =   ((x',x'':'b.  ((rep(x')) = (rep(x'')))(x' = x''))   ((x:'a. ((P(x)) = (x':'b. (x = (rep(x')))))))

1 step

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