Nuprl - Proof: hsum ty def 1 2

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hsum ty def 1 2

1. 'a : S
2. 'b : S
3. x : hbool

hbool
4. (

u:'a+'b. (f =

(rep_sum(u))))(x)

x':hsum('a; 'b). x = rep_sum(x')

hbool

By:	Simpsetp [`hol_to_nuprl`] THEN StrongAuto

Generated subgoals:

None

About:

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