Nuprl - Proof: hit sum wd

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hit sum wd

and

(equal(it_sum(nil),0)

,all

h:hnum. all(

t:hlist(hnum). equal(it_sum(cons(h,t)),add(h,it_sum(t))))))

By:

Generated subgoals:

None

About:

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