let u := td _ _ iej
case intro
α : Type u_1
inst✝ : DecidableEq α
h : α
t : List α
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) }
left✝ : (List.all t fun x => x != h) = true
tdiff : differs t = true
td : DifferentList t := correctLeft t tdiff
⊢ i = j
case intro
α : Type u_1
inst✝ : DecidableEq α
h : α
t : List α
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) }
left✝ : (List.all t fun x => x != h) = true
tdiff : differs t = true
td : DifferentList t := correctLeft t tdiff
u : { val := i, isLt := (_ : Nat.succ i ≤ List.length t) } = { val := j, isLt := (_ : Nat.succ j ≤ List.length t) } :=
  td { val := i, isLt := List.get._sunfold.proof_1 h t i ilt } { val := j, isLt := List.get._sunfold.proof_1 h t j jlt }
    iej
⊢ i = j