proposition: Lemma environment_bindE (E A B : UU0) (M := EnvironmentMonad.acto E) (m : M A) (f : A -> M B) : m >>= f = fun e => f (m e) e.
proof: Proof. by []. Qed.
imports: mathcomp(all_ssreflect) imonae_lib HB(structures) ihierarchy imonad_lib ifail_lib istate_lib itrace_lib imonad_transformer