En este trabajo presentamos la base fundamental de un método para probar propiedades inductivas de programas funcionales: la inducción por reescritura. El método propuesto es una especialización del principio general de inducción noetheriana donde la relación bien fundada es la relación de reescritura de un sistema terminante. Se demuestra la corrección de esta forma de inducción con una definición particular de conjunto de cobertura adaptada a los sistemas de reescritura de términos originados en programas funcionales que terminan. Se plantea la utilización de lemas auxiliares para recuperar demostraciones que no pueden continuar exclusivamente por el mecanismo de inducción por reescritura. Nuestra experiencia con el asistente de prueba p3f [7] ha mostrado la utilidad del método para la demostración de teoremas sobre propiedades de programas funcionales.