IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
hsum ty def13 1. 'a : S
2. 'b : S
3. x : hbool'a'bhbool
4. x':hsum('a; 'b). x = rep_sum(x')
(f:'a'b. u:'a+'b. (f = (rep_sum(u))))(x)
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
'a
x':hsum('a; 'b). x = rep_sum(x')
(
f:
u:'a+'b. (f =
