proposition: Lemma cgetmkrlistC A T T1 (r : loc T) r1 l k : cchk r >> (mkrlist T1 l r1 >>= (fun r' => cget r >>= k r')) = cget r >>= (fun v => mkrlist T1 l r1 >>= k ^~ v) :> M A.
proof: Proof. elim: l k => [|a l IH] k /=. under [in RHS]eq_bind do rewrite bindretf. by rewrite !bindretf cchkget. symmetry. under eq_bind do rewrite bindA. rewrite -IH. under [mkrlist _ _ _ >>= _]eq_bind do rewrite -cchknewget. by rewrite cchkmkrlistC bindA. Qed.
imports: ZArith mathcomp(all_ssreflect) infotheo(ssrZ) monad_model HB(structures) monae_lib hierarchy monad_lib typed_store_lib