∀ {α : Type u_2} {β : Type u_1} (T_t' : Finset β) (f_t' : β → Set α) (T_s : Finset β) (f_s : β → Set α) (a : α),
  ((∀ i ∈ T_s, a ∈ f_s i) ∧ ∀ i ∈ T_t', a ∈ f_t' i) ↔
    ∀ (i : β),
      i ∈ T_s ∨ i ∈ T_t' →
        a ∈ if i ∈ T_s then if i ∈ T_t' then f_s i ∩ f_t' i else f_s i else if i ∈ T_t' then f_t' i else ∅