no goals
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a a' : α
b' : β a'
l : List (Sigma β)
⊢ a ∈ keys (kinsert a' b' l) ↔ a = a' ∨ a ∈ keys l
by_cases h : a = a' <;> simp [h]