1. 'a : S
2. 'b : S
3. f : hbool  'a  'b  hbool
4. v1 : 'a
5. 'b
6. f = (b:hbool. x:'a. y:'b. (x = v1)b)
  u:'a+'b. f = rep_sum(u)  'a'b

By:	Subst (f = (b:. x:'a. y:'b. (x = v1)b)) 0

1

u:'a+'b. (b:. x:'a. y:'b. (x = v1)b) = rep_sum(u)  'a'b

1 step

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