No encuentro la forma de definir en coq lo que quiero probar.
Quiero probar que (add 0 (S 0) empty) es del tipo array(0+1).
[] |- (add 0 (S 0) empty): array(0+1)
Como se escribe para iniciar la demostracion?
Saludos.
Hola.
No hay que probar nada acá, sino simplemente calcular el tipo con Check.
Saludos, Carlos