proposition: Lemma output_bindE (L A B : UU0) (M := OutputMonad.acto L) (m : M A) (f : A -> M B) : m >>= f = let: (x, w) := m in let: (x', w') := f x in (x', w ++ w').
proof: Proof. by []. Qed.
imports: mathcomp(all_ssreflect) imonae_lib HB(structures) ihierarchy imonad_lib ifail_lib istate_lib itrace_lib imonad_transformer