fact: Definition M := [the typedStoreMonad ml_type _ monad_model.locT_nat of acto ml_type].
imports: ZArith mathcomp(all_ssreflect) infotheo(ssrZ) monad_model HB(structures) monae_lib hierarchy monad_lib typed_store_lib PrimInt63 typed_store_model