proposition: Lemma refin_bind_guard {M : plusMonad} A (b : bool) (m1 m2 : M A) : (b -> m2 `<=` m1) -> guard b >> m2 `<=` guard b >> m1.
proof: Proof. case: b => [h|_]; first by apply: refin_bindl => -[]; exact: h. by rewrite guardF !bindfailf; exact: refin_refl. Qed.
imports: mathcomp(all_ssreflect) imonae_lib HB(structures) ihierarchy imonad_lib Equations(Equations)