case cons head tail HInd =>
byCases Hname: head.fst = name <;> try assumption
have ⟨headName, headτ, headVal⟩ := head; simp at *
intros H; cases H
simp;
α σ : 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
⊢ (if head.fst = name then some head.2 else getT name tail) = some { fst := τ, snd := v } →
    (if head.fst = name then
        if h : head.2.fst = τ then
          some
            (cast
              (_ :
                (match head.2.fst with
                  | MLIRType.float a => Float
                  | MLIRType.int signedness sz => FinInt sz
                  | MLIRType.tensor1d => Tensor1D
                  | MLIRType.tensor2d => Tensor2D
                  | MLIRType.tensor4d => Tensor4D
                  | MLIRType.index => ℤ
                  | MLIRType.undefined a => Unit
                  | MLIRType.extended σ => ε σ
                  | MLIRType.erased => Unit) =
                  match τ with
                  | MLIRType.float a => Float
                  | MLIRType.int signedness sz => FinInt sz
                  | MLIRType.tensor1d => Tensor1D
                  | MLIRType.tensor2d => Tensor2D
                  | MLIRType.tensor4d => Tensor4D
                  | MLIRType.index => ℤ
                  | MLIRType.undefined a => Unit
                  | MLIRType.extended σ => ε σ
                  | MLIRType.erased => Unit)
              head.2.snd)
        else none
      else get name tail τ) =
      some v
no goals