proposition: Lemma crunnewchkC A T1 T2 (m : M A) (r : A -> loc T1) s : crun (m >>= fun x => cchk (r x)) -> crun (m >>= fun x => cnew T2 (s x) >> cchk (r x)).
proof: Proof. rewrite crunchkget => Hck. under eq_bind do rewrite -bindA. rewrite -bindA crunmskip. exact: crunnewgetC. Qed.
imports: ssrmatching Reals JMeq mathcomp(all_ssreflect) infotheo(Reals_ext) monae_lib hierarchy