m : Type u → Type u_1
α β σ : Type u
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : StateT σ m α
y : StateT σ m β
s : σ
⊢ run
      (do
        let a ← x
        let _ ← y
        pure a)
      s =
    do
    let p ← run x s
    let p' ← run y p.snd
    pure (p.fst, p'.snd)
m : Type u → Type u_1
α β σ : Type u
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : StateT σ m α
y : StateT σ m β
s : σ
⊢ run (SeqLeft.seqLeft x fun x => y) s = do
    let p ← run x s
    let p' ← run y p.snd
    pure (p.fst, p'.snd)
show (x >>= fun a => y >>= fun _ => pure a).run s = _
no goals
m : Type u → Type u_1
α β σ : Type u
inst✝¹ : Monad m
inst✝ : LawfulMonad m
x : StateT σ m α
y : StateT σ m β
s : σ
⊢ run
      (do
        let a ← x
        let _ ← y
        pure a)
      s =
    do
    let p ← run x s
    let p' ← run y p.snd
    pure (p.fst, p'.snd)
simp