. case cons h t => 
  unfold DifferentList
  intros i j iej
  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
case cons
α : Type u_1
inst✝ : DecidableEq α
head✝ : α
tail✝ : List α
p : differs (head✝ :: tail✝) = true
⊢ DifferentList (head✝ :: tail✝)
no goals