no goals
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s✝ : Finmap β
s : AList β
h : ¬a ∈ ⟦s⟧
⊢ (insert a b ⟦s⟧).entries = { fst := a, snd := b } ::ₘ ⟦s⟧.entries
simp [AList.insert_entries_of_neg (mt mem_toFinmap.1 h), -insert_entries]