unfold DifferentList
α : Type u_1
inst✝ : BEq α
xs : List α
x : α
xxs : DifferentList (x :: xs)
⊢ DifferentList xs
α : Type u_1
inst✝ : BEq α
xs : List α
x : α
xxs : DifferentList (x :: xs)
⊢ ∀ (i j : Fin (List.length xs)), List.get xs i = List.get xs j → i = j