∀ {α : Type u_1} {p : α → Prop} {r : { a // p a } → { a // p a } → Prop} (h : ∀ x ∈ [], p x),
  List.IsChain r ([].attachWith p h) ↔ List.IsChain (fun a b => ∃ (ha : p a) (hb : p b), r ⟨a, ha⟩ ⟨b, hb⟩) []