simp [*]
case h.inl
name₁ name₂ : String
val₁ val₂ : ℕ
s : State
hneq : name₁ ≠ name₂
name' : String
h : name' = name₁
⊢ State.update name₁ val₁ (State.update name₂ val₂ s) name' = State.update name₂ val₂ (State.update name₁ val₁ s) name'
no goals