apply dedup_eq_of_rel
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ xs : List α
i j : xs.Index
h : Setoid.r i.val j.val
⊢ dedup s i = dedup s j
case h
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ xs : List α
i j : xs.Index
h : Setoid.r i.val j.val
⊢ Setoid.r i.val (dedup s j).val