Il existe deux manières habituelles de présenter un système de types dépendants, une qui utilise une notion de calcul indépendante du typage, tel que la beta-reduction, et une autre qui introduit une notion de jugements d'égalité typée directement dans les règles de typage du système. La question de savoir si ces deux présentations décrivaient la même théorie est restée un problème pendant plusieurs années. Adams a fait un premier vers une réponse à cette question en la prouvant correcte pour une classe de Systèmes de Types Pures (PTS) dit "fonctionnels". Dans ce papier, nous étendons encore un peu plus la preuve d'Adams en prouvant que cette équivalence est vraie pour tout les Systèmes de Types Pures "semi-complet", en combinant les idées présentées par Adams avec une étude de la forme générale des types dans les PTS. Ce résultat est un premier pas vers une extension à des systèmes de types contenant du sous-typage, ce qui permettrait de rapprocher encore plus la méta-théorie de certains assistants à la preuve , tel que Coq, de leur implémentation.