case mk rName rArgs rOps =>
intros args env res env' H env₂ Henv₂
simp [denoteRegion] at *; simp_monad at *
(split at H <;> try contradiction); rename_i argsR HargsR
have ⟨argsR, argsEnv⟩ := argsR; cases argsR
have ⟨argsEnv₂, HargsEnv₂, HdenoteArgs⟩ := denoteTypedArgs_equiv HargsR Henv₂
rw [HdenoteArgs]; simp at *
apply denoteOps_equiv (by assumption) (by assumption)
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
rName : String
rArgs : List (TypedSSAVal Δ)
rOps : List (Op Δ)
⊢ ∀ ⦃args : TypedArgs Δ⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
    denoteRegion Δ (Region.mk rName rArgs rOps) args env = Except.ok (res, env') →
      ∀ ⦃env₂ : SSAEnv Δ⦄,
        SSAEnv.equiv env env₂ →
          ∃ env₂',
            SSAEnv.equiv env' env₂' ∧ denoteRegion Δ (Region.mk rName rArgs rOps) args env₂ = Except.ok (res, env₂')
no goals