* 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