proposition: Lemma list_bindE (A B : UU0) (M := ListMonad.acto) (m : M A) (f : A -> M B) : m >>= f = flatten (map f m).
proof: Proof. by []. Qed.
imports: mathcomp(all_ssreflect) imonae_lib HB(structures) ihierarchy imonad_lib ifail_lib istate_lib itrace_lib imonad_transformer