next ha =>
  split
  next h =>
    rw [eqNdrec_symm] at h
    rw [h, val_ndrec]
  next h =>
    rw [eqNdrec_symm] at h
    rw [h, val_ndrec, val_tail, val_tail, ih]
case cons.isFalse
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : (List.dedup s xs).Index), (undedup s i).val = i.val
i : (List.dedup s (x :: xs)).Index
h✝ : ¬Logic.Any (List.map (Setoid.r x) xs)
⊢ (match ⋯ ▸ i with
      | head => head
      | i.tail => (undedup s i).tail).val =
    i.val
no goals