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

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
args : TypedArgs Δ
env : SSAEnv Δ
name : String
formals : List (TypedSSAVal Δ)
ops : List (Op Δ)
⊢ run (denoteRegion Δ (Region.mk name formals ops) args) env =
    run
      (do
        denoteTypedArgs args (List.map Prod.fst formals)
        denoteOps Δ ops)
      env
Tactic:
simp[denoteRegion]
State after:
no goals