no goals
α : Type u
β : α → Type v
l✝ l₁ l₂ : List (Sigma β)
inst✝ : DecidableEq α
a : α
s : Sigma β
tail✝ : List (Sigma β)
l : List (Sigma β)
⊢ kunion (kerase a (s :: tail✝)) (kerase a l) = kerase a (kunion (s :: tail✝) l)
by_cases h : a = s.1 <;> simp [h, kerase_comm a s.1 l, kunion_kerase]