Ce projet propose une traduction automatique d'une partie de la bibliothèque HOL-Light vers le système Rocq. Il permet d'aligner des types et fonctions mathématiques entre ces deux environnements de preuve formelle, facilitant ainsi l'utilisation de théorèmes HOL-Light dans Rocq. L'objectif est d'accélérer le développement de preuves formelles en exploitant des résultats déjà établis dans HOL-Light, tout en garantissant leur compatibilité avec Rocq.