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. rewrite bindA. rewrite -[LHS]cnewchk. under eq_bind => r1. rewrite bindA; under eq_bind do rewrite !bindA. under cchknewE => r2 r1r2. rewrite bindretf bindA bindretf. rewrite bindA cputget. rewrite bindretf. rewrite -bindA. rewrite cputgetC //. over. rewrite cnewget. over. rewrite cnewchk. under [RHS]eq_bind do (rewrite bindA; under eq_bind do rewrite bindretf). done. Qed.
imports: ZArith mathcomp(all_ssreflect) infotheo(ssrZ) monad_model HB(structures) monae_lib hierarchy monad_lib typed_store_lib