intro p
α : Type u_1
de : DecidableEq α
x : α
xs : List α
i : Fin (List.length xs)
d : differs (x :: xs) = true
⊢ ¬x = List.get xs i
α : 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