∀ {ι : Type u_2} {α : Type u_4} {β : Type u_5} (r : α → β → Prop) [inst : (a : α) → DecidablePred (r a)]
  [inst_1 : DecidableEq α] [inst_2 : DecidableEq β] (s : Finset α) (t : Finset ι) (f : ι → Finset β),
  Rel.interedges r s (t.biUnion f) = t.biUnion fun b => Rel.interedges r s (f b)