proposition: Lemma guard_isNondet (b : bool) : plus_isNondet (guard b : M _).
proof: Proof. exists (if b then ndRet tt else @ndFail _). by case: ifP; rewrite (guardT, guardF). Qed.
imports: mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy monad_lib Equations(Equations)