next h => rw [dedup, dif_neg ha, eqNdrec_symm, ←h]
case h_1
α : 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)
x✝ : (x :: List.dedup s xs).Index
heq✝ : ⋯ ▸ i = head
⊢ dedup s head = i

case h_2
α : 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)
x✝ : (x :: List.dedup s xs).Index
i✝ : (List.dedup s xs).Index
heq✝ : ⋯ ▸ i = i✝.tail
⊢ dedup s (undedup s i✝).tail = i
case h_2
α : 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)
x✝ : (x :: List.dedup s xs).Index
i✝ : (List.dedup s xs).Index
heq✝ : ⋯ ▸ i = i✝.tail
⊢ dedup s (undedup s i✝).tail = i