Theorem: SSAScope.get_set_ne_val
Proof state before:
case cons.h1
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v : SSAVal
τ τ' : MLIRType δ
val : MLIRType.eval τ
head : SSAVal × (τ : MLIRType δ) × MLIRType.eval τ
nil : List (SSAVal × (τ : MLIRType δ) × MLIRType.eval τ)
Hne : head.fst ≠ v
tail_ih✝ : get v (set head.fst τ val nil) τ' = get v nil τ'
⊢ (if head.fst = v then
      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)
            val)
      else none
    else get v nil τ') =
    if head.fst = v 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 v nil τ'

case cons.h2
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
Hne : v' ≠ v
τ τ' : MLIRType δ
val : MLIRType.eval τ
head : SSAVal × (τ : MLIRType δ) × MLIRType.eval τ
nil : List (SSAVal × (τ : MLIRType δ) × MLIRType.eval τ)
tail_ih✝ : get v (set v' τ val nil) τ' = get v nil τ'
H : ¬head.fst = v'
⊢ (if head.fst = v 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 v (set v' τ val nil) τ') =
    if head.fst = v 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 v nil τ'
Tactic:
. simp [Hne]
Proof state after:
case cons.h2
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
Hne : v' ≠ v
τ τ' : MLIRType δ
val : MLIRType.eval τ
head : SSAVal × (τ : MLIRType δ) × MLIRType.eval τ
nil : List (SSAVal × (τ : MLIRType δ) × MLIRType.eval τ)
tail_ih✝ : get v (set v' τ val nil) τ' = get v nil τ'
H : ¬head.fst = v'
⊢ (if head.fst = v 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 v (set v' τ val nil) τ') =
    if head.fst = v 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 v nil τ'