proposition: Lemma mkrlist_drop A T l r k : (mkrlist T l r >>= fun r' => rdrop (size l) r' >>= k r') = (mkrlist T l r >>= k ^~ r) :> M A.
proof: Proof. elim/last_ind: l r k => [|a l IH] r k. by rewrite !bindretf. rewrite -cats1 mkrlist_cat size_cat bindA /= bindretf. under eq_bind do under eq_bind do rewrite rdrop_add -bindA bindmret bindA. rewrite -cnewchk. under eq_bind => r1. rewrite IH. under [mkrlist _ _ _ >>= _]eq_bind do rewrite bindA. rewrite cgetmkrlistC. over. rewrite cnewget /= -[cnew _ >>= _]bindA. by under eq_bind do rewrite bindretf. Qed.
imports: ZArith mathcomp(all_ssreflect) infotheo(ssrZ) monad_model HB(structures) monae_lib hierarchy monad_lib typed_store_lib