. case succ j => 
  simp [List.get] at iej
  simp
  simp [differs] at p
  cases p with | intro _ tdiff =>
  let td := correctLeft t tdiff        
  let u := td _ _ iej
  simp at u
  assumption
case succ
α : Type u_1
inst✝ : DecidableEq α
h : α
t : List α
p : differs (h :: t) = true
i : Nat
ilt : Nat.succ i < List.length (h :: t)
n✝ : Nat
jlt : Nat.succ n✝ < List.length (h :: t)
iej : List.get (h :: t) { val := Nat.succ i, isLt := ilt } = List.get (h :: t) { val := Nat.succ n✝, isLt := jlt }
⊢ Nat.succ i = Nat.succ n✝
no goals