Buenas,
Estoy trancado en este ejercicio y tambien en el 7.3. Al probar llego a este contexto y obligaciones de prueba. No se cual es el camino correcto para avanzar.
estas son las tacticas hasta el momento:
intros.
apply xIFelse.
apply eboolf.
inversion_clear H.
gracias
Hola.
Notar que el primer subgoal sale con inversiones esencialmente, primero en H0 y luego en la que se genera a partir de esta. Se prueba ya que true no evalúa a false.
En general, cuando hay tipos inductivos instanciados en constructores, con inversion se determinan las condiciones para que esto ocurra. Según el caso hay que aplicar más de una vez inversion (cuando hay varios contructores). Tener cuidado con inversion_clear si no se refleja el efecto en las hipótesis involucradas. Sino, aplicar inversion que deja las igualdades.
Saludos, Carlos
Hola.
El 7.2 sale esencialmente con inversion, ya que Execute está instanciada y lo que hay que hacer es ir hacia atrás instanciando lo necesario para demsotrar lo pedido.
No tiene sentido que aparezca acá por ejemplo LExecute. Vos hiciste inducción? Sino, no veo de donde sale el primer contexto que mostrás.
Saludos, Carlos