Theorem: HMem.Memory.getm_setv (HMem/Memory/Basic.lean)

State before:
m : Memory
v : Bool
⊢ getm (setv m v) = getm m
Tactic:
funext b
State after:
case h
m : Memory
v b : Bool
⊢ getm (setv m v) b = getm m b

State before:
case h
m : Memory
v b : Bool
⊢ getm (setv m v) b = getm m b
Tactic:
cases b <;> simp
State after:
no goals