cases H : StateT.run ma env
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
a b : Type
Δ : Dialect α σ ε
ma : TopM Δ a
k : a → TopM Δ b
env : SSAEnv Δ
⊢ (do
      let p ← StateT.run ma env
      StateT.run (k p.fst) p.snd) =
    match StateT.run ma env with
    | Except.ok (a, env') => StateT.run (k a) env'
    | Except.error e => Except.error e
case error
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
a b : Type
Δ : Dialect α σ ε
ma : TopM Δ a
k : a → TopM Δ b
env : SSAEnv Δ
a✝ : String × SSAEnv Δ
H : StateT.run ma env = Except.error a✝
⊢ (do
      let p ← Except.error a✝
      StateT.run (k p.fst) p.snd) =
    match Except.error a✝ with
    | Except.ok (a, env') => StateT.run (k a) env'
    | Except.error e => Except.error e

case ok
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
a b : Type
Δ : Dialect α σ ε
ma : TopM Δ a
k : a → TopM Δ b
env : SSAEnv Δ
a✝ : a × SSAEnv Δ
H : StateT.run ma env = Except.ok a✝
⊢ (do
      let p ← Except.ok a✝
      StateT.run (k p.fst) p.snd) =
    match Except.ok a✝ with
    | Except.ok (a, env') => StateT.run (k a) env'
    | Except.error e => Except.error e