push_neg
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T T₁ T₂ : Theory α
⊢ ¬¬(L)-Consistent (T₁ ∪ T₂) → ¬(¬(L)-Consistent T₁ ∨ ¬(L)-Consistent T₂)
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T T₁ T₂ : Theory α
⊢ (L)-Consistent (T₁ ∪ T₂) → (L)-Consistent T₁ ∧ (L)-Consistent T₂