assumption
case h2
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
name : SSAVal
τ : MLIRType δ
v : MLIRType.eval τ
head : SSAVal × (τ : MLIRType δ) × MLIRType.eval τ
tail : List (SSAVal × (τ : MLIRType δ) × MLIRType.eval τ)
HInd : getT name tail = some { fst := τ, snd := v } → get name tail τ = some v
Hname : ¬head.fst = name
⊢ getT name tail = some { fst := τ, snd := v } → get name tail τ = some v
no goals