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