simp
case cons
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v : SSAVal
τ : MLIRType δ
val : MLIRType.eval τ
head : SSAVal × (τ : MLIRType δ) × MLIRType.eval τ
tail : List (SSAVal × (τ : MLIRType δ) × MLIRType.eval τ)
tail_ih✝ : getT v (set v τ val tail) = some { fst := τ, snd := val }
⊢ getT v (set v τ val (head :: tail)) = some { fst := τ, snd := val }
case cons
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v : SSAVal
τ : MLIRType δ
val : MLIRType.eval τ
head : SSAVal × (τ : MLIRType δ) × MLIRType.eval τ
tail : List (SSAVal × (τ : MLIRType δ) × MLIRType.eval τ)
tail_ih✝ : getT v (set v τ val tail) = some { fst := τ, snd := val }
⊢ getT v (if head.fst = v then (head.fst, { fst := τ, snd := val }) :: tail else head :: set v τ val tail) =
    some { fst := τ, snd := val }