fact: Definition step3 B cr (m : M B) := m >> do uds <- get ; let (b, uds') := test cr uds in put uds' >> guard b.
imports: ZArith mathcomp(all_ssreflect) infotheo(ssrZ) monae_lib hierarchy monad_lib fail_lib state_lib