Equivalence, morphisme et réécriture en Coq Où l’on apprend comment étendre le fonctionnement de la tactique `rewrite` coq preuve méthodes formelles
