contradiction
case inl
α : Type u_1
inst✝ : DecidableEq α
x y : α
xs : List α
hneq : x ≠ y
hmem : x = y
⊢ (match decide ¬x ∈ [y] with
    | true => x :: filter (fun x => decide ¬x ∈ [y]) xs
    | false => filter (fun x => decide ¬x ∈ [y]) xs) =
    x :: filter (fun x => decide ¬x ∈ [y]) xs
no goals