proposition: Lemma cchknewE T1 T2 (r1 : loc T1) s (A : UU0) (k1 k2 : loc T2 -> M A) : (forall r2 : loc T2, loc_id r1 != loc_id r2 -> k1 r2 = k2 r2) -> cchk r1 >> (cnew T2 s >>= k1) = cchk r1 >> (cnew T2 s >>= k2).
proof: Proof. move=> Hk; rewrite !(bindA,bindskipf); exact: cgetnewE. Qed.
imports: ssrmatching Reals JMeq mathcomp(all_ssreflect) infotheo(Reals_ext) monae_lib hierarchy