proposition: Lemma puttselectC (x : S) A (s : seq A) B (f : _ -> M B) : put x >> (tselect s >>= f) = tselect s >>= (fun rs => put x >> f rs).
proof: Proof. elim: s f => [|h t IH] f. by rewrite tselect_nil 2!bindfailf bindmfail. case: t IH f => [|h' t] IH f. by rewrite tselect1 !bindretf. rewrite tselect_cons // => H. rewrite [in LHS]alt_bindDl [in RHS]alt_bindDl alt_bindDr. congr (_ [~] _); first by rewrite 2!bindretf. rewrite 2!bindA IH; bind_ext => y; by rewrite !bindretf. Qed.
imports: mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy monad_lib fail_lib