rw [val_ndrec]
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : xs.Index), Setoid.r i.val (dedup s i).val
i : (x :: xs).Index
h✝ : ¬Logic.Any (List.map (Setoid.r x) xs)
⊢ Setoid.r head.val
    (let_fun this := ⋯;
      ⋯ ▸ head).val
α : Type u_1
s : Setoid α
inst✝ : DecidableRel Setoid.r
xs✝ : List α
x : α
xs : List α
ih : ∀ (i : xs.Index), Setoid.r i.val (dedup s i).val
i : (x :: xs).Index
h✝ : ¬Logic.Any (List.map (Setoid.r x) xs)
⊢ Setoid.r head.val head.val