apply funext
name₁ name₂ : String
val₁ val₂ : ℕ
s : State
hneq : name₁ ≠ name₂
⊢ State.update name₁ val₁ (State.update name₂ val₂ s) = State.update name₂ val₂ (State.update name₁ val₁ s)
case h
name₁ name₂ : String
val₁ val₂ : ℕ
s : State
hneq : name₁ ≠ name₂
⊢ ∀ (x : String),
    State.update name₁ val₁ (State.update name₂ val₂ s) x = State.update name₂ val₂ (State.update name₁ val₁ s) x