rw [dedup, dif_pos ha, ih, eqNdrec_symm]
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : (List.dedup s xs).Index), dedup s (undedup s i) = i
i : (List.dedup s (x :: xs)).Index
ha : Logic.Any (List.map (Setoid.r x) xs)
⊢ dedup s (undedup s (⋯ ▸ i)).tail = i
no goals