induction scope with
| nil =>
  simp; simp [Hne, Hne.symm]
  simp [equiv]; intros name τ''
  byCases Hv: v' = name
  byCases Hτ: τ' = τ'' <;> simp [Hne.symm]
| cons head tail Hind =>
  simp [equiv] at *
  intros name; specialize Hind name
  simp at *
  byCases Hv': head.fst = v' <;> simp [Hne]
  byCases Hv: head.fst = v <;> simp [Hv']
  byCases Hname: head.fst = name <;> assumption
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
Hne : v' ≠ v
scope : SSAScope δ
τ τ' : MLIRType δ
val : MLIRType.eval τ
val' : MLIRType.eval τ'
⊢ equiv (set v τ val (set v' τ' val' scope)) (set v' τ' val' (set v τ val scope))
no goals