let h1 := xxs i1 j1
case a
α : Type u_1
inst✝ : BEq α
xs : List α
x : α
xxs : DifferentList (x :: xs)
i j : Fin (List.length xs)
iej : List.get xs i = List.get xs j
i1 : Fin (List.length (x :: xs)) := appendFin x xs i
j1 : Fin (List.length (x :: xs)) := appendFin x xs j
⊢ i.val = j.val
case a
α : Type u_1
inst✝ : BEq α
xs : List α
x : α
xxs : DifferentList (x :: xs)
i j : Fin (List.length xs)
iej : List.get xs i = List.get xs j
i1 : Fin (List.length (x :: xs)) := appendFin x xs i
j1 : Fin (List.length (x :: xs)) := appendFin x xs j
h1 : List.get (x :: xs) i1 = List.get (x :: xs) j1 → i1 = j1 := xxs i1 j1
⊢ i.val = j.val