Découverte de lemmes par instanciation de métavariables dans les preuves par récurrence.