induction scope <;> simp
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
name : SSAVal
scope : SSAScope δ
τ : MLIRType δ
v : MLIRType.eval τ
⊢ getT name scope = some { fst := τ, snd := v } → get name scope τ = some v
case cons
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
name : SSAVal
τ : MLIRType δ
v : MLIRType.eval τ
head✝ : SSAVal × (τ : MLIRType δ) × MLIRType.eval τ
tail✝ : List (SSAVal × (τ : MLIRType δ) × MLIRType.eval τ)
tail_ih✝ : 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