Des familles inductives de types de données servent bien à représenter le lambda-calcul: le paramètre de la famille décrit l'ensemble de noms de variables libres admises, et le changement du paramètre au cours de la récurrence reflète la génération de noms pour les variables liées. Cette représentation satisfait les propriétés de base de la substitution, dictées par la théorie des catégories. C'est bien connu.
On veut aller plus loin: On encapsule des sous-expressions de lambda-termes comme si elles n'étaient que des noms de variables libres. Ceci donne le lambda-calcul avec aplatissement explicite (une forme de substitution explicite). Sa représentation par une famille inductive requièrt des principes d'induction qui ne sont offertes par aucun assistant de preuves, or elles pouvaient être encodées dans Coq. Là, déjà la notion d'une occurrence libre d'une variable est un défi pour la conception mathématique.
Heureusement, la vérification entière se fait dans Coq, le plus grand problème étant un affaiblissement de la règle que la substitution qui remplace chaque variable par le terme qui consiste de cette variable n'a aucun effet. En plus, toute notre théorie axiomatique est justifiée dans le calcul des constructions inductives avec insignifiance des preuves.