fact: Definition AppM {A B} (f : M (A -> M B)) (x : A) := do f <- f; f x.
imports: ZArith mathcomp(all_ssreflect) infotheo(ssrZ) monad_model HB(structures) monae_lib hierarchy monad_lib typed_store_lib PrimInt63 typed_store_model