case Ret ret =>
  unfold OpM.toTopM; unfold OpM.toTopM at H
  cases H <;> simp
  exists env₂
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
regions : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
Hregs : denoteRegionsEquivInvariant regions
ret : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' : SSAEnv Δ
H : toTopM regions (Ret ret) env = Except.ok (res, env')
env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
⊢ ∃ env₂', SSAEnv.equiv env' env₂' ∧ toTopM regions (Ret ret) env₂ = Except.ok (res, env₂')
no goals