Hola
Sobre lo primero una opción es usar: Load State.
Sobre lo segundo, sugerimos no usar Maps. Para funciones parciales en State.v está:
(* Shortcut notation for partial functions *)
Definition partial a b := a -> option b.
Notation "a ⇸ b" := (partial a b) (at level 51, right associativity).
(* NOTA: Con esto no es necesario usar Maps.v mencionado en el práctico 7 *)
Saludos, Carlos