proposition: Lemma perm3 T (s1 s2 s3 s4 : coq_type N T) : do r1 <- cnew s1; do r2 <- cnew s2; do r3 <- cnew s3; cput r1 s4 = do r1 <- cnew s4; do r2 <- cnew s2; do r3 <- cnew s3; skip :> M _.
proof: Proof. rewrite -cnewchk. under eq_bind do rewrite -cchknewC -[cput _ _]bindmskip 2!cchknewput. by rewrite cnewput. Qed.
imports: ZArith mathcomp(all_ssreflect) infotheo(ssrZ) monad_model HB(structures) monae_lib hierarchy monad_lib typed_store_lib