∀ {α : Type u_1} {β : Type u_2} {p : α → Prop} {xs : Array { x // p x }} {f : { x // p x } → β → β} {g : α → β → β}
  {x : β}, (∀ (x : α) (h : p x) (b : β), f ⟨x, h⟩ b = g x b) → Array.foldr f x xs = Array.foldr g x xs.unattach