induction scope with
| nil => simp;
| cons head nil =>
  simp
  byCases H: head.fst = v <;> try apply cast_eq
  assumption
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v : SSAVal
scope : SSAScope δ
τ : MLIRType δ
val : MLIRType.eval τ
⊢ get v (set v τ val scope) τ = some val
no goals