rw [get_to_getT]
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
name : SSAVal
scope : SSAScope δ
τ : MLIRType δ
v : MLIRType.eval τ
⊢ get name scope τ = some v → getT name scope = some { fst := τ, snd := v }
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
name : SSAVal
scope : SSAScope δ
τ : MLIRType δ
v : MLIRType.eval τ
⊢ (match getT name scope 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) =
      some v →
    getT name scope = some { fst := τ, snd := v }