∀ {α : Type u_1} {P : α → Prop} {xs : Array (Subtype P)} {f : α → Bool},
  Array.filter f xs.unattach =
    (Array.filter
        (fun x =>
          match x with
          | ⟨x, h⟩ => binderNameHint x f (binderNameHint h () (f (wfParam x))))
        xs).unattach