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