'a,'b:S.
  all
  (e:'b. equal
  (e:'b. (inr(e)
  (e:'b. ,abs_sum(b:hbool. x:'a. y:'b. and(equal(y,e),not(b)))))

1

1. 'a : S 2. 'b : S 3. e : 'b   inr(e) = abs_sum(b:hbool. x@0:'a. y:'b. (y = e)b)

3 steps

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