no goals
m : Type u_1 → Type u_2
σ α β : Type u_1
inst✝ : Monad m
x : StateT σ m α
f : α → StateT σ m β
s : σ
⊢ run (x >>= f) s = do
    let p ← run x s
    run (f p.fst) p.snd
simp [bind, StateT.bind, run]