rw [val_tail]
α : 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
ha : Logic.Any (List.map (Setoid.r x) xs)
this : List.dedup s (x :: xs) = List.dedup s xs
⊢ (undedup s (⋯ ▸ i)).tail.val = i.val
α : 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
ha : Logic.Any (List.map (Setoid.r x) xs)
this : List.dedup s (x :: xs) = List.dedup s xs
⊢ (undedup s (⋯ ▸ i)).val = i.val