proposition: Lemma crunchkput A T (m : M A) (r : A -> loc T) s : crun (m >>= fun x => cchk (r x)) -> crun (m >>= fun x => cput (r x) (s x)).
proof: Proof. rewrite crunchkget; exact: crungetput. Qed.
imports: ssrmatching Reals JMeq mathcomp(all_ssreflect) infotheo(Reals_ext) monae_lib hierarchy