∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] (𝒜 ℬ : Finset (Finset α)) (s : Finset α),
  ((𝒜 ∪ ℬ).truncatedInf s).card + ((𝒜 ⊻ ℬ).truncatedInf s).card = (𝒜.truncatedInf s).card + (ℬ.truncatedInf s).card