simp[remove]
α✝ : Type u
inst✝³ : DecidableEq α✝
β✝ : Type v
inst✝² : DecidableEq β✝
m : Type ?u.181446 → Type ?u.181448
α : Type u_1
β : Type ?u.181454
inst✝¹ : Monad m
inst✝ : DecidableEq α
l : List α
a : α
⊢ remove a (a :: l) = remove a l
no goals