proposition: Lemma putgetput (S : UU0) {M : stateMonad S} x {B} (k : _ -> M B) : put x >> get >>= (fun x' => k x') = put x >> k x :> M _.
proof: Proof. by rewrite putget bindA bindretf. Qed.
imports: mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy monad_lib fail_lib