assumption
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
val : List SSAVal
env₁ : SSAEnv Δ
r : Unit
env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env₁ env₂
⊢ SSAEnv.equiv env₁ env₂
no goals