proposition: Lemma bind_ext_guard {M : failMonad} (A : UU0) (b : bool) (m1 m2 : M A) : (b -> m1 = m2) -> guard b >> m1 = guard b >> m2.
proof: Proof. by case: b => [->//|_]; rewrite guardF !bindfailf. Qed.
imports: mathcomp(all_ssreflect) imonae_lib HB(structures) ihierarchy imonad_lib Equations(Equations)