proposition: Lemma cchkput T (r : loc T) (s : coq_type N T) : cchk r >> cput r s = cput r s.
proof: Proof. by rewrite bindA bindskipf cgetput. Qed.
imports: ssrmatching Reals JMeq mathcomp(all_ssreflect) infotheo(Reals_ext) monae_lib hierarchy