proposition: Lemma rhd_tl_tl_is_true : crun (do l <- cycle ml_bool true false; do l1 <- rtl l; do l2 <- rtl l1; rhd ml_bool false l2) = Some true.
proof: Proof. rewrite -rhd_is_true -[in RHS]rtl_tl_self [in RHS]bindA. under [in RHS]eq_bind do rewrite bindA. done. Qed.
imports: ZArith mathcomp(all_ssreflect) infotheo(ssrZ) monad_model HB(structures) monae_lib hierarchy monad_lib typed_store_lib