intro h
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T T₁ T₂ : Theory α
⊢ (∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₁ ∪ T₂) → L ⊬! Γ.conj' ⟶ ⊥) →
    (∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₁) → L ⊬! Γ.conj' ⟶ ⊥) ∧
      ∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₂) → L ⊬! Γ.conj' ⟶ ⊥
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T T₁ T₂ : Theory α
h : ∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₁ ∪ T₂) → L ⊬! Γ.conj' ⟶ ⊥
⊢ (∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₁) → L ⊬! Γ.conj' ⟶ ⊥) ∧
    ∀ {Γ : List (Formula α)}, (∀ p ∈ Γ, p ∈ T₂) → L ⊬! Γ.conj' ⟶ ⊥