* modify type check in order to be nearer from the documentation
* important details in compositionnality lemma are wrong in our typing system. But I think subject reduction is still true without this lemma in this particular case
* begin proof of progress
* commit before merge