Uncurry transformation and proof

[zoep]

Right now the uncurry transformation and its proof relies on John Li's framework that automatically derives transformations (and proofs) from the specification. But:

• The framework is part of the ANF pipeline. This is a big dependency that we have to maintain and none of us really knows how it works.

• The uncurry transformation and its proof is derived automatically. It is hard to modify and maintain without knowledge of the above.

So it would be nice to have a simple uncurry transformation and the corresponding proof, by done hand.