(17steps total) PrintForm Definitions Lemmas hol sum Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hsum iso def 1 2
1. 'a : S
2. 'b : S
  iso_pair('a+'b;'a'b;is_sum_rep;rep_sum;abs_sum)
By: Unab [`iso_pair`;`habs_sum`;`his_sum_rep`] THEN HN THEN StrongAuto
THEN
Try (Complete (Unfold `label` 0))

Generated subgoals:

1 3. r : 'a'b
  (@u:'a+'b. (rep_sum(u) = r  'a'b))
  =
  (@a:'a+'b. (r = rep_sum(a)  'a'b))
1 step
2   type_definition('a'b;'a+'b;f:'a'b. u:'a+'b
  type_definition('a'b;'a+'b;f:'a'b. (f
  type_definition('a'b;'a+'b;f:'a'b. = (rep_sum
  type_definition('a'b;'a+'b;f:'a'b. = ((u)));rep_sum)
12 steps

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

(17steps total) PrintForm Definitions Lemmas hol sum Sections HOLlib Doc