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

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