case cons head tail HInd =>
unfold getT get
byCases Hname: head.fst = name
case h2 =>
  rw [HInd]
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
name : SSAVal
τ : MLIRType δ
head : SSAVal × (τ : MLIRType δ) × MLIRType.eval τ
tail : List (SSAVal × (τ : MLIRType δ) × MLIRType.eval τ)
HInd :
  get name tail τ =
    match getT name tail with
    | none => none
    | some { fst := τ', snd := v' } =>
      if H : τ' = τ then
        some
          (cast
            (_ :
              (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) =
                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)
            v')
      else none
⊢ get name (head :: tail) τ =
    match getT name (head :: tail) with
    | none => none
    | some { fst := τ', snd := v' } =>
      if H : τ' = τ then
        some
          (cast
            (_ :
              (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) =
                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)
            v')
      else none
no goals