Hola, en un momento en una prueba llego a que: S (length A l) <> 0.
¿ Se puede usar el axioma discNat: forall n:nat, S n <> 0 ?
Si, aunque se puede probar (por inducción) como un lema auxiliar.
Saludos, Carlos
Hola, en un momento en una prueba llego a que: S (length A l) <> 0.
¿ Se puede usar el axioma discNat: forall n:nat, S n <> 0 ?
Si, aunque se puede probar (por inducción) como un lema auxiliar.
Saludos, Carlos