fact: Definition opdot (a : A) (m : M (seq B)) : M (seq B) := get >>= (fun st => guard (ok (op st a)) >> put (op st a) >> fmap (res a) m).
imports: mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy monad_lib fail_lib