fact: Definition bind (e : M ~~> N) := forall (A B : UU0) (m : M A) (f : A -> M B), e B (m >>= f) = e A m >>= (e B \o f).
imports: mathcomp(all_ssreflect) imonae_lib HB(structures) ihierarchy imonad_lib ifail_lib istate_lib