(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
  'a,'b:S.
  all
  (f:hbool
  ( 'a
  ( 'b
  ( hbool. equal
  ( hbool. (is_sum_rep(f)
  ( hbool. ,exists
  ( hbool. ,(v1:'a. exists
  ( hbool. ,(v1:'a. (v2:'b. or
  ( hbool. ,(v1:'a. (v2:'b. (equal
  ( hbool. ,(v1:'a. (v2:'b. ((f
  ( hbool. ,(v1:'a. (v2:'b. (,b:hbool. x:'a. y:'b. and(equal(x,v1),b))
  ( hbool. ,(v1:'a. (v2:'b. ,equal
  ( hbool. ,(v1:'a. (v2:'b. ,(f
  ( hbool. ,(v1:'a. (v2:'b. ,,b:hbool. x:'a. y:'b. and
  ( hbool. ,(v1:'a. (v2:'b. ,,b:hbool. x:'a. y:'b. (equal(y,v2)
  ( hbool. ,(v1:'a. (v2:'b. ,,b:hbool. x:'a. y:'b. ,not(b))))))))
By: Unab [`his_sum_rep`] THEN Simpsetp [`hol_to_nuprl`] THEN StrongAuto

Generated subgoal:

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
8 steps

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

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