proposition: Lemma cchk_mkrlist_put_drop A T l (r r1 : loc (ml_rlist T)) f k : cchk r >> (mkrlist T l r1 >>= fun r' => cput r (f r') >> (rdrop (size l) r' >>= k r')) = cchk r >> (mkrlist T l r1 >>= fun r' => rdrop (size l) r' >>= (fun r'' => cput r (f r') >> k r' r'')) :> M A.
proof: Proof. elim/last_ind: l r1 k => [|a l IH] r1 k. by rewrite !bindretf. rewrite -cats1 mkrlist_cat size_cat /=. under eq_bind do rewrite bindretf bindA. rewrite -cchknewC. under cchknewE => r2 rr2. under [mkrlist _ _ _ >>= _]eq_bind do rewrite rdrop_add bindA. rewrite IH mkrlist_drop /=. under [mkrlist _ _ _ >>= _]eq_bind do rewrite !bindA -[cput _ _ >> _]bindA cputgetC //. under eq_bind do under eq_bind do under eq_bind do rewrite !bindretf. over. rewrite cchknewC. symmetry. under eq_bind do rewrite bindretf bindA. under [LHS]cchknewE => r2 rr2. under eq_bind do rewrite rdrop_add bindA. rewrite mkrlist_drop /=. under eq_bind do rewrite /rtl bindmret /= bindA. under eq_bind do under eq_bind do rewrite bindretf. over. done. Qed.
imports: ZArith mathcomp(all_ssreflect) infotheo(ssrZ) monad_model HB(structures) monae_lib hierarchy monad_lib typed_store_lib