m : Type u_1 → Type u_2
σ α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : StateT σ m α
y : StateT σ m β
s : σ
⊢ run
      (do
        let _ ← x
        y)
      s =
    do
    let p ← run x s
    run y p.snd
m : Type u_1 → Type u_2
σ α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : StateT σ m α
y : StateT σ m β
s : σ
⊢ run (SeqRight.seqRight x fun x => y) s = do
    let p ← run x s
    run y p.snd
show (x >>= fun _ => y).run s = _
no goals
m : Type u_1 → Type u_2
σ α β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : StateT σ m α
y : StateT σ m β
s : σ
⊢ run
      (do
        let _ ← x
        y)
      s =
    do
    let p ← run x s
    run y p.snd
simp