fact: Definition dassert (p : pred A) a : M { a | p a } := if Bool.bool_dec (p a) true is left pa then Ret (exist _ _ pa) else fail.
imports: mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy monad_lib Equations(Equations)