proposition: Lemma cchkputC T1 T2 (r1 : loc T1) (r2 : loc T2) (s : coq_type N T2) : cchk r1 >> cput r2 s = cput r2 s >> cchk r1.
proof: Proof. by rewrite bindA bindskipf cgetputC bindA. Qed.
imports: ssrmatching Reals JMeq mathcomp(all_ssreflect) infotheo(Reals_ext) monae_lib hierarchy