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

State before:
name name' : String
val : ℕ
s : State
hneq : name' ≠ name
⊢ State.update name val s name' = s name'
Tactic:
apply if_neg
State after:
case hnc
name name' : String
val : ℕ
s : State
hneq : name' ≠ name
⊢ ¬name' = name

State before:
case hnc
name name' : String
val : ℕ
s : State
hneq : name' ≠ name
⊢ ¬name' = name
Tactic:
assumption
State after:
no goals