no goals
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b : β a
s : AList β
h : ¬a ∈ s
⊢ (insert a b s).entries = { fst := a, snd := b } :: s.entries
rw [insert_entries, kerase_of_not_mem_keys h]