proposition: Lemma cchkgetC T1 T2 (r1: loc T1) (r2: loc T2) (A: UU0) (k: coq_type N T2 -> M A) : cchk r1 >> (cget r2 >>= k) = cget r2 >>= (fun s => cchk r1 >> k s).
proof: Proof. under [in RHS]eq_bind do rewrite bindA bindskipf. by rewrite !(bindA,bindskipf) cgetC. Qed.
imports: ssrmatching Reals JMeq mathcomp(all_ssreflect) infotheo(Reals_ext) monae_lib hierarchy