case a
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b b' : β a
s : AList β
⊢ (insert a b' (insert a b s)).entries = (insert a b' s).entries
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b b' : β a
s : AList β
⊢ insert a b' (insert a b s) = insert a b' s
ext : 1
no goals
case a
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
b b' : β a
s : AList β
⊢ (insert a b' (insert a b s)).entries = (insert a b' s).entries
simp only [AList.insert_entries, List.kerase_cons_eq]