simp[H, bind, Except.bind]
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
β : Type
Δ : Dialect α σ ε
ma : TopM Δ Unit
mb : TopM Δ β
env : SSAEnv Δ
out : Unit × SSAEnv Δ
H : StateT.run ma env = Except.ok out
⊢ (do
      let p ← Except.ok out
      StateT.run mb p.snd) =
    match Except.ok out with
    | Except.ok (PUnit.unit, env') => StateT.run mb env'
    | Except.error e => Except.error e
no goals