Please do not merge this code.

It is clearly a PLE thing.

Both MA (prior this commit) and upstream Sprite (at the time of this
commit) had bug in type renaming where parameters were renamed but
not references to them in termination metric. All tests "appeared to
work" simply because the code used same (formal) parameter names in both
type signature and function declaration.

However in general case they do not need to be the same. Solution is
simple - also rename parameters in termination metric.

…g tail elimination of EIf

Now L8 test_abs_* pass.

The code was actually malformed because metric referred to function's
formal parameter (not parameter in signature!)

test_abs_03 and test_abs_04 are just like test_abs_02 except they use
bitvectors instead of int.

We shall write a meaningful one when the time comes.

The prover found a subtle bug!

…icit refinement

NB: This is NOT the neg test illustrating Issue#265