proposition: Lemma refin_bindl (M : prePlusMonad) A B (m : M A) (f g : A -> M B) : (f `<.=` g) -> (m >>= f `<=` m >>= g).
proof: Proof. by move=> fg; rewrite /refin -alt_bindDr; bind_ext => a; exact: fg. Qed.
imports: mathcomp(all_ssreflect) imonae_lib HB(structures) ihierarchy imonad_lib Equations(Equations)