Hola,
Varias consultas, primero las pruebas tanto para beval como sbeval me quedaron exactamente iguales; para ambas utilize un lema auxiliar L: beval e = true \/ beval = f. Me parece que no es la idea, ya que como consecuencia de esto, los programas generados tambien quedan identicos.
Con respecto a la parte 3, supongo que la idea es utilizar Hint Constructors BEval y utilizar la tactica auto; haciendo esto no obtuve demasiada ayuda (solo me sirvio para probar el caso base de BEval), alguna sugerencia?
Gracias,
Carlos.