proposition: Lemma cgetchk T (r : loc T) (A: UU0) (k : coq_type N T -> M A) : cget r >>= (fun s => cchk r >> k s) = cget r >>= k.
proof: Proof. under eq_bind do rewrite bindA bindskipf; by rewrite cgetget. Qed.
imports: ssrmatching Reals JMeq mathcomp(all_ssreflect) infotheo(Reals_ext) monae_lib hierarchy