Hola,
No sé cómo hay que definir Memoria, yo la definí cómo:
Definition Memoria := nat -> Valor.
Parameter LookUp : ...
Sin embargo con estas definiciones no se me ocurre cómo hacer en el ejercicio 6.3 para definir update. ¿La idea es simplemente un parámetro con el tipo y después axiomas?
Parameter update : Memoria -> nat -> Valor -> Memoria.
Saludos,
Jairo.