Typing of expressions is done. However, there are still some admits in the proofs, to be fixed in the following days.