RA2017: Ejercicios de cuantificadores sobre listas en Isabelle/HOL

En la primera parte de la clase de hoy del curso de Razonamiento automático se han comentado las soluciones de la 4ª relación de ejercicios sobre cuantificadores sobre listas en Isabelle/HOL.

La teoría con las soluciones de los ejercicios es la siguiente