rw [eqNdrec_symm] at hj
α : 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
h : Setoid.r x j✝.val
ha : ¬Logic.Any (List.map (Setoid.r x) xs)
this : List.dedup s (x :: xs) = x :: List.dedup s xs
j : (List.dedup s xs).Index
hj : this ▸ j✝ = j.tail
⊢ head = ⋯ ▸ j✝
α : 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
h : Setoid.r x j✝.val
ha : ¬Logic.Any (List.map (Setoid.r x) xs)
this : List.dedup s (x :: xs) = x :: List.dedup s xs
j : (List.dedup s xs).Index
hj : j✝ = ⋯ ▸ j.tail
⊢ head = ⋯ ▸ j✝