proposition: Lemma putselectC (x : S) A (s : seq A) B (f : A * (seq A) -> M B) : put x >> (select s >>= f) = select s >>= (fun rs => put x >> f rs).
proof: Proof. rewrite selectE {1}fmapE. under eq_bind do rewrite bindA. rewrite puttselectC [in RHS]fmapE bindA. by bind_ext => x0; rewrite 2!bindretf. Qed.
imports: mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy monad_lib fail_lib