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

State before:
name : String
val : ℕ
s : State
⊢ State.update name val s name = val
Tactic:
apply if_pos
State after:
case hc
name : String
val : ℕ
s : State
⊢ name = name

State before:
case hc
name : String
val : ℕ
s : State
⊢ name = name
Tactic:
rfl
State after:
no goals