induction xs with
| nil => contradiction
| cons x xs ih =>
  simp only [undedup]
  split
  next ha => rw [dedup, dif_pos ha, ih, eqNdrec_symm]
  next ha =>
    split
    next h => rw [dedup, dif_neg ha, eqNdrec_symm, ←h]
    next h => rw [dedup, dif_neg ha, eqNdrec_symm, ih, ←h]
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ xs : List α
i : (List.dedup s xs).Index
⊢ dedup s (undedup s i) = i
no goals