next ha =>
  have : (x :: xs).dedup s = x :: xs.dedup s := if_neg ha
  rw [eqNdrec_symm]
  match hj : this ▸ j with
  | head =>
    rw [eqNdrec_symm] at hj
    rw [hj, val_ndrec, val_head] at h
    absurd ha
    apply Logic.Any.of_index (i.map (s.r x))
    rw [val_map]
    symmetry
    exact h
  | tail j =>
    rw [eqNdrec_symm] at hj
    rw [hj, val_ndrec, val_tail] at h
    rw [hj, ih h]
    elim_casts
case isFalse
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ {i : xs.Index} {j : (List.dedup s xs).Index}, Setoid.r i.val j.val → dedup s i = j
i✝ : (x :: xs).Index
j : (List.dedup s (x :: xs)).Index
i : xs.Index
h : Setoid.r i.val j.val
h✝ : ¬Logic.Any (List.map (Setoid.r x) xs)
⊢ (let_fun this := ⋯;
    ⋯ ▸ (dedup s i).tail) =
    j
no goals