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

State before:
ma₀ ma₁ m : Memory
b : Bool
bs : List Bool
⊢ setmp (setmp m (b :: bs) ma₀) (b :: bs) ma₁ = setmp m (b :: bs) ma₁
Tactic:
simp [setmp_setmp (bs := bs)]
State after:
no goals