constructor
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ xs : List α
i : xs.Index
j : (List.dedup s xs).Index
⊢ dedup s i = j ↔ Setoid.r i.val j.val
case mp
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ xs : List α
i : xs.Index
j : (List.dedup s xs).Index
⊢ dedup s i = j → Setoid.r i.val j.val

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