cases Classical.em (name' = name₁) with
| inl h => simp [*]
| inr h =>
  cases Classical.em (name' = name₁) with
  | inl h => simp [*]
  | inr h => simp [State.update, *]
case h
name₁ name₂ : String
val₁ val₂ : ℕ
s : State
hneq : name₁ ≠ name₂
name' : String
⊢ State.update name₁ val₁ (State.update name₂ val₂ s) name' = State.update name₂ val₂ (State.update name₁ val₁ s) name'
no goals