simp [appendFin] at i1ej1
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 xs { val := i.val, isLt := (_ : Nat.succ i.val ≤ List.length xs) } =
    List.get xs { val := j.val, isLt := (_ : Nat.succ j.val ≤ List.length xs) } →
  appendFin x xs i = appendFin x xs j :=
  xxs i1 j1
i1ej1 : appendFin x xs i = appendFin x xs j := h1 iej
⊢ 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 xs { val := i.val, isLt := (_ : Nat.succ i.val ≤ List.length xs) } =
    List.get xs { val := j.val, isLt := (_ : Nat.succ j.val ≤ List.length xs) } →
  appendFin x xs i = appendFin x xs j :=
  xxs i1 j1
i1ej1 : i.val = j.val
⊢ i.val = j.val