theorem Array.attachWith_unattach {a : Type u} {p : a → Prop} (arr : Array (Subtype p)) (h : ∀ (x : a), x ∈ arr.unattach → p x) : arr.unattach.attachWith p h = arr