cases d with | intro all _ =>
let une := listAllCorrect i all
simp [bne, BEq.beq] at une
let une := of_decide_eq_false une
rw [p] at une
contradiction
α : 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) = true ∧ differs xs = true
⊢ False
no goals