Theorem: run_TopM_denoteRegionsByIx_cons (MLIR/Semantics/Semantics.lean)

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
ix : ℕ
r : TypedArgs Δ → TopM Δ (TypedArgs Δ)
rs : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
args : TypedArgs Δ
env : SSAEnv Δ
⊢ run (TopM.denoteRegionsByIx (r :: rs) ix args) env =
    run
      (match ix with
      | 0 => r args
      | Nat.succ ix' => TopM.denoteRegionsByIx rs ix' args)
      env
Tactic:
simp[TopM.denoteRegionsByIx]
State after:
no goals