proposition: Lemma cchknewC T1 T2 (r : loc T1) s (A : UU0) (k : loc T2 -> M A) : cchk r >> (cnew T2 s >>= fun r' => cchk r >> k r') = cchk r >> (cnew T2 s >>= k).
proof: Proof. rewrite !(bindA,bindskipf). under eq_bind do under eq_bind do rewrite bindA. rewrite cgetnewD. by under eq_bind do under eq_bind do rewrite bindskipf. Qed.
imports: ssrmatching Reals JMeq mathcomp(all_ssreflect) infotheo(Reals_ext) monae_lib hierarchy