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