Theorem: LoVe.update_same_const (LoVe/LoVelib.lean)

State before:
name : String
val : ℕ
⊢ (State.update name val fun x => val) = fun x => val
Tactic:
apply funext
State after:
case h
name : String
val : ℕ
⊢ ∀ (x : String), State.update name val (fun x => val) x = val

State before:
case h
name : String
val : ℕ
⊢ ∀ (x : String), State.update name val (fun x => val) x = val
Tactic:
simp [State.update]
State after:
no goals