Coq en Coq ? Mécaniser la logique d'un assistant à la démonstration