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