Hola.
Una alternativa es usar como mappings las funciones de Coq, tal como sugerí ayer en un mail (con tipo option como retorno, para totalizar funciones parciales).
No obstante, te pongo abajo un ejemplo de uso de map_apply para definir (de cierta manera - es solo un ejemplo) la precondición de la acción chmod:
Definition PreConditionChmod (s : state) : Prop :=
aos_activity s = waiting /\
exists os,
Value _ os = map_apply os_ident_eq (oss s) (active_os s) /\
(hcall os) = None.
Saludos, Carlos