proposition: Lemma crunchkget A T (m : M A) (r : A -> loc T) : crun (m >>= fun x => cchk (r x)) = crun (m >>= fun x => cget (r x)) :> bool.
proof: Proof. by rewrite /cchk -bindA crunmskip. Qed.
imports: ssrmatching Reals JMeq mathcomp(all_ssreflect) infotheo(Reals_ext) monae_lib hierarchy