proposition: Lemma rhd_is_true : crun (do l <- cycle ml_bool true false; rhd ml_bool false l) = Some true.
proof: Proof. rewrite bindA. under eq_bind do rewrite !bindA. under eq_bind do under eq_bind do rewrite !bindA bindretf !bindA bindretf cputget. rewrite -bindA_uncurry -bindA crunret // crunchkput // bindA. under eq_bind do rewrite !bindA. under eq_bind do under eq_bind do rewrite bindretf /=. by rewrite crunnewchkC // crunnewchk0. Qed.
imports: ZArith mathcomp(all_ssreflect) infotheo(ssrZ) monad_model HB(structures) monae_lib hierarchy monad_lib typed_store_lib