fact: Definition bindX X Y (t : MX X) (f : X -> MX Y) : MX Y := t >>= fun c => match c with inl z => Ret (inl z) | inr x => f x end.
imports: mathcomp(all_ssreflect) imonae_lib HB(structures) ihierarchy imonad_lib ifail_lib istate_lib