(9steps total) PrintForm Definitions hol sum Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: his sum rep wd 1 2
1. 'a : S
2. 'b : S
3. f : hbool  'a  'b  hbool
4. v1:'a, v2:'b.
4. f = (b:hbool. x:'a. y:'b. (x = v1)b)
4.  f = (b:hbool. x@0:'a. y:'b. (y = v2)b)
  u:'a+'b. f = rep_sum(u)  'a'b
By: Lasts 3 Analyze THEN StrongAuto

Generated subgoals:

1 4. v1 : 'a
5. 'b
6. f = (b:hbool. x:'a. y:'b. (x = v1)b)  (hbool  'a  'b  hbool)
  u:'a+'b. f = rep_sum(u)  'a'b
2 steps
2 4. 'a
5. v2 : 'b
6. f = (b:hbool. x@0:'a. y:'b. (y = v2)b)  (hbool  'a  'b  hbool)
  u:'a+'b. f = rep_sum(u)  'a'b
1 step

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

(9steps total) PrintForm Definitions hol sum Sections HOLlib Doc