assumption
case h2.a
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
env₁ env₂ : SSAEnv δ
HEnv : equiv env₁ env₂
name : SSAVal
τ : MLIRType δ
v : MLIRType.eval τ
name' : SSAVal
τ' : MLIRType δ
Hname : ¬name = name'
⊢ name ≠ name'
no goals