Translating pairwise relations on sets to lists

On a list with no duplicates, the condition of Set.Pairwise and List.Pairwise are equivalent.

theorem List.Nodup.pairwise_of_set_pairwise {α : Type u_1} {l : List α} {r : α → α → Prop} (hl : l.Nodup) (h : {x : α | x ∈ l}.Pairwise r) : Pairwise r l

@[simp]

theorem List.Nodup.pairwise_coe {α : Type u_1} {r : α → α → Prop} {l : List α} [Std.Symm r] (hl : l.Nodup) : {a : α | a ∈ l}.Pairwise r ↔ Pairwise r l