simp [Hne, Hne.symm]
case nil
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
Hne : v' ≠ v
τ τ' : MLIRType δ
val : MLIRType.eval τ
val' : MLIRType.eval τ'
⊢ equiv
    (if v' = v then [(v', { fst := τ, snd := val })]
    else [(v', { fst := τ', snd := val' }), (v, { fst := τ, snd := val })])
    (if v = v' then [(v, { fst := τ', snd := val' })]
    else [(v, { fst := τ, snd := val }), (v', { fst := τ', snd := val' })])
case nil
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
Hne : v' ≠ v
τ τ' : MLIRType δ
val : MLIRType.eval τ
val' : MLIRType.eval τ'
⊢ equiv [(v', { fst := τ', snd := val' }), (v, { fst := τ, snd := val })]
    [(v, { fst := τ, snd := val }), (v', { fst := τ', snd := val' })]