cases i with | mk iv ilt =>
cases j with | mk jv jlt => 
apply Fin.eq_of_val_eq
simp
cases iv 
. cases jv
  simp
  case succ j => 
    simp [List.get] at iej
    let xs := differsHead p iej
    contradiction                
. case succ i => 
  cases jv
  . simp [List.get] at iej
    let xs := differsHead p iej.symm
    contradiction
  . 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
α : Type u_1
inst✝ : DecidableEq α
h : α
t : List α
p : differs (h :: t) = true
i j : Fin (List.length (h :: t))
iej : List.get (h :: t) i = List.get (h :: t) j
⊢ i = j
no goals