proposition: Lemma cnewchk T s (A : UU0) (k : loc T -> M A) : cnew T s >>= (fun r => cchk r >> k r) = cnew T s >>= k.
proof: Proof. under eq_bind do rewrite bindA. rewrite cnewget. by under eq_bind do rewrite bindskipf. Qed.
imports: ssrmatching Reals JMeq mathcomp(all_ssreflect) infotheo(Reals_ext) monae_lib hierarchy