proposition: Lemma rnth_is_true n : crun (do l <- cyclel ml_bool true (nseq n false); rnth ml_bool false n.+1 l) = Some true.
proof: Proof. rewrite /cyclel !bindA -cnewchk. under eq_bind => r. rewrite [(mkrlist _ _ _ >>= _) >>= _]bindA -add1n /rnth. under [mkrlist _ _ _ >>= _]eq_bind do rewrite bindA bindretf rdrop_add /= bindA bindmret bindA cputget bindretf. rewrite -{2}(size_nseq n false). rewrite cchk_mkrlist_put_drop mkrlist_drop. under [mkrlist _ _ _ >>= _]eq_bind do rewrite cputget. rewrite -!bindA. over. rewrite -bindA crunret // -bindA_uncurry crunchkput // bindA. under eq_bind => r. rewrite bindA. under eq_bind do rewrite bindretf /= -[cchk _]bindmskip. rewrite bindA cchkmkrlistC. over. rewrite cnewchk -bindA crunmskip. elim: n => /= [|n IH]. by rewrite bindmret crunnew0. by rewrite -bindA crunnew. Qed.
imports: ZArith mathcomp(all_ssreflect) infotheo(ssrZ) monad_model HB(structures) monae_lib hierarchy monad_lib typed_store_lib