intros Hne scope τ val
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
⊢ v' ≠ v → ∀ ⦃scope : SSAScope δ⦄ ⦃τ : MLIRType δ⦄ ⦃val : MLIRType.eval τ⦄, getT v (set v' τ val scope) = getT v scope
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
Hne : v' ≠ v
scope : SSAScope δ
τ : MLIRType δ
val : MLIRType.eval τ
⊢ getT v (set v' τ val scope) = getT v scope