Drafty definition of the unfolding
Merge branch 'master' lemmas of Marcelo

- conflicts solved in 04-unfoldings.tex
- new lemmas to prove