proposition: Lemma cchknewput T T' (r : loc T) s s' (A : UU0) k : cchk r >> (cnew T' s' >>= fun r' => cput r s >> k r') = cput r s >> (cnew T' s' >>= k) :> M A.
proof: Proof. by rewrite bindA bindskipf cputnewC. Qed.
imports: ssrmatching Reals JMeq mathcomp(all_ssreflect) infotheo(Reals_ext) monae_lib hierarchy