assumption
α : Type u_1
inst✝ : BEq α
x y : α
xs : List α
dl : DifferentList (x :: y :: xs)
i j : Fin (List.length (y :: x :: xs))
iej : List.get (x :: y :: xs) (shuffleIndex i) = List.get (x :: y :: xs) (shuffleIndex j)
siej : shuffleIndex i = shuffleIndex j := dl (shuffleIndex i) (shuffleIndex j) iej
ssiej : i = j
⊢ i = j
no goals