unfold differs at d
α : Type u_1
de : DecidableEq α
x : α
xs : List α
i : Fin (List.length xs)
d : differs (x :: xs) = true
p : x = List.get xs i
⊢ False
α : Type u_1
de : DecidableEq α
x : α
xs : List α
i : Fin (List.length xs)
p : x = List.get xs i
d : ((List.all xs fun x_1 => x_1 != x) && differs xs) = true
⊢ False