DSification relation.
Free variable generation in cps transform.
No more several vvars.
Mold is NOT broken.
First proven version.
Small simplifications.
Minor changes.
Merge branch 'dsify-nov'
On going fixes for the full proof.