proposition: Lemma state_bindE (S A B : UU0) (M := StateMonad.acto S) (m : M A) (f : A -> M B) : m >>= f = uncurry f \o m.
proof: Proof. by []. Qed.
imports: mathcomp(all_ssreflect) imonae_lib HB(structures) ihierarchy imonad_lib ifail_lib istate_lib itrace_lib imonad_transformer