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