fact: Fixpoint sem {M : nondetMonad} {A} (m : t A) : M A := match m with | ret A a => Ret a | bind A B m f => sem m >>= (sem \o f) | fail A => hierarchy.fail | alt A m1 m2 => sem m1 [~] sem m2 end.
imports: mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy monad_lib Equations(Equations)