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

State before:
m : Memory
b : Bool
ma : Memory
⊢ getm (setm m b ma) b = ma
Tactic:
cases b <;> simp
State after:
no goals