contradiction
case intro
α : Type u_1
de : DecidableEq α
x : α
xs : List α
i : Fin (List.length xs)
p : x = List.get xs i
all : (List.all xs fun x_1 => x_1 != x) = true
right✝ : differs xs = true
une✝ : decide (List.get xs i = x) = false
une : ¬List.get xs i = List.get xs i
⊢ False
no goals