proposition: Lemma cchkC T1 T2 (r1 : loc T1) (r2 : loc T2) : cchk r1 >> cchk r2 = cchk r2 >> cchk r1.
proof: Proof. by rewrite !(bindA,bindskipf) cgetC. Qed.
imports: ssrmatching Reals JMeq mathcomp(all_ssreflect) infotheo(Reals_ext) monae_lib hierarchy