First working version of the ForAll transformation. Still need to be cleaned and debugged. Test4.scala shows that it works (at least for a very simple case).