∀ {ι : Type v} [inst : DecidableEq ι] {α : ι → Type u} {δ : (i : ι) → α i → Type w}
  [inst_1 : (i : ι) → (j : α i) → AddCommMonoid (δ i j)] (f : DirectSum ι fun i => DirectSum (α i) fun j => δ i j)
  (i : ι) (j : α i), (DirectSum.sigmaUncurry f) ⟨i, j⟩ = (f i) j