progress on (re-)proving the sum example

The specification looks much better. The only flaw is the ```.Exps``` that I cannot get rid of right now.

@andreistefanescu please review