no goals
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
s✝ : Finmap β
s : AList β
⊢ (erase a (erase a' ⟦s⟧)).entries = (erase a' (erase a ⟦s⟧)).entries
simp only [AList.erase_erase, erase_toFinmap]