simp
α : Type u_1
inst✝ : DecidableEq α
h : α
t : List α
p : differs (h :: t) = true
i : Nat
ilt : Nat.succ i < List.length (h :: t)
j : Nat
jlt : Nat.succ j < List.length (h :: t)
iej :
  List.get t { val := i, isLt := (_ : Nat.succ i ≤ List.length t) } =
    List.get t { val := j, isLt := (_ : Nat.succ j ≤ List.length t) }
⊢ Nat.succ i = Nat.succ j
α : Type u_1
inst✝ : DecidableEq α
h : α
t : List α
p : differs (h :: t) = true
i : Nat
ilt : Nat.succ i < List.length (h :: t)
j : Nat
jlt : Nat.succ j < List.length (h :: t)
iej :
  List.get t { val := i, isLt := (_ : Nat.succ i ≤ List.length t) } =
    List.get t { val := j, isLt := (_ : Nat.succ j ≤ List.length t) }
⊢ i = j