Def rep_sum
Def == u:'a+'b. InjCase(u
Def == u:'a+'b. InjCase; p. b:. x:'a. y:'b. (x = p)b
Def == u:'a+'b. InjCase; q. b:. x:'a. y:'b. (y = q)b)

is mentioned by

Thm* 'a,'b:S, u,v:'a+'b. rep_sum(u) = rep_sum(v)  'a'b  u = v	[hrep_sum_inj]
Thm* 'a,'b:S. Thm* (x:'a+'b. abs_sum(rep_sum(x)) = x  'a+'b) Thm* & (x:('a'b). is_sum_rep(x) = ((rep_sum(abs_sum(x))) = x))	[sum_iso]
Thm* 'a,'b:S. Thm* and Thm* (all(a:hsum('a; 'b). equal(abs_sum(rep_sum(a)),a)) Thm* ,all Thm* ,(r:hbool  'a  'b  hbool. equal Thm* ,(r:hbool  'a  'b  hbool. (is_sum_rep(r) Thm* ,(r:hbool  'a  'b  hbool. ,equal(rep_sum(abs_sum(r)),r))))	[hsum_iso_def]
Def is_sum_rep == f:'a'b. u:'a+'b. (f = (rep_sum(u)))	[his_sum_rep]
Def abs_sum == f:'a'b. @u:'a+'b. (rep_sum(u) = f  'a'b)	[habs_sum]

Try larger context: HOLlib IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html