proposition: Lemma _rtl_tl_self T (a b : coq_type N T) : do l <- cycle T a b; do l1 <- rtl l; rtl l1 = cycle T a b.
proof: Proof. rewrite /cycle bindA -[LHS]cnewchk. under eq_bind => r1. rewrite bindA; under eq_bind do rewrite !bindA. under cchknewE do rewrite bindretf bindA bindretf bindA cputget bindretf -bindA cputgetC //. rewrite cnewget; over. rewrite cnewchk. by under [RHS]eq_bind do (rewrite bindA; 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