∀ {α : Type u_1} {β : Type u_2} {inst : DecidableEq α} [inst_1 : DecidableEq α] [inst_2 : CommSemiring β]
  (𝒜 𝒜_1 : Finset (Finset α)),
  𝒜 = 𝒜_1 →
    ∀ (a a_1 : α),
      a = a_1 →
        ∀ (f f_1 : Finset α → β),
          f = f_1 → ∀ (s s_1 : Finset α), s = s_1 → collapse✝ 𝒜 a f s = collapse✝¹ 𝒜_1 a_1 f_1 s_1