fact: Definition bindO A B (m : MO A) (f : A -> MO B) : MO B := m >>= (fun o => let: (x, w) := o in f x >>= (fun o' => let (x', w') := o' in Ret (x', w ++ w'))).
imports: mathcomp(all_ssreflect) imonae_lib HB(structures) ihierarchy imonad_lib ifail_lib istate_lib