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