match REGIONS: regions with
| .nil =>
  intros region HregIn args env res env' H env₂ Henv₂
  contradiction
| .cons head tail =>
  intros region HregIn args env res env' H env₂ Henv₂
  simp [TopM.mapDenoteRegion] at HregIn
  cases HregIn
  case inl HXX =>
    subst HXX;
    sorry
    case inr HXX =>
    apply mapDenoteRegion_equiv <;> assumption
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
regions : List (Region Δ)
⊢ denoteRegionsEquivInvariant (TopM.mapDenoteRegion Δ regions)
no goals