Add the theorem on constraint typing
Finish to model the main document structure. Proof are pending.