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

In prior sections: hol sum

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