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

1	inr(e) = abs_sum(rep_sum(inr(e)))  'a+'b	1 step
2	4. inr(e) = abs_sum(rep_sum(inr(e)))  'a+'b   inr(e) = abs_sum(b:hbool. x@0:'a. y:'b. (y = e)b)	1 step

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