On trouve dans cet article une traduction possible de la notion de termes et de substitution dans le calcul des constructions avec types inductifs et une preuve constructive de l'unification au premier ordre de laquelle on peut extraire un algorithme (proche de celui de Robinson). Le logiciel utilise pour le codage et la vérification des preuves est le Coq Proof Assistant version 5.6. L'article est conçu pour une lecture en parallèle du code en Coq et de la transcription qui en est faite en langage mathématique. Il a été écrit également dans le but d'aider ceux qui le désirent à pénétrer rapidement dans le monde du calcul des constructions.