no goals
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b b' : β a
⊢ (insert a b (singleton a b')).entries = (singleton a b).entries
simp only [AList.insert_entries, List.kerase_cons_eq, and_self_iff, AList.singleton_entries,
  heq_iff_eq, eq_self_iff_true]