Buenas,
Una consulta, es correcto definir las pre y post condiciones de manera idnuctiva como de la siguiente manera:
Inductive Pre : State -> Action -> Prop :=
|pre_read : forall....... -> Pre s (read va)
etc...
Porque no queremos errarle a eso,
Gracias!