Buenas,
Para definir update utilice beq_nat de la librería Arith.EqNat.
Luego para la parte 5 utilice el lema beq_nat_eq de esa misma librería.
Me quedo muy fácil, así que quería consultar si puedo utilizar la librería o tengo que definir mi propia igualdad booleana entre naturales.
Saludos.