proposition: Lemma crunnewchk0 T s : crun (cnew T s >>= fun r => cchk r : M _).
proof: Proof. by rewrite -(bindskipf (_ >>= _)) crunnewchk // crunskip. Qed.
imports: ssrmatching Reals JMeq mathcomp(all_ssreflect) infotheo(Reals_ext) monae_lib hierarchy