(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
1. 'a : S
2. 'b : S
3. f : hbool  'a  'b  hbool
  (u:'a+'b. (f = (rep_sum(u))))
  =
  (v1:'a
  (v2:'b
  (((f = (b:hbool. x:'a. y:'b. (x = v1)b))
  ( (f = (b:hbool. x:'a. y:'b. (y = v2)b))))
   hbool
By: Simpsetp [`bequal`] THEN StrongAuto

Generated subgoals:

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

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