simp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : ¬(L)-Consistent insert p T ∧ ¬(L)-Consistent insert (~p) T
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ T
Δ : List (Formula α)
hΔ₁ : ∀ p ∈ Δ, p ∈ T
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
hΔ₂ : L ⊢! ~p ⋏ Δ.conj' ⟶ ⊥
this✝ : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
this : L ⊬! (Γ ++ Δ).conj' ⟶ ⊥
⊢ ∀ p ∈ Γ ++ Δ, p ∈ T
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
L : DeductionParameter α
inst✝ : L.Normal
T : Theory α
consisT : (L)-Consistent T
p : Formula α
hC : ¬(L)-Consistent insert p T ∧ ¬(L)-Consistent insert (~p) T
Γ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ, p ∈ T
Δ : List (Formula α)
hΔ₁ : ∀ p ∈ Δ, p ∈ T
hΓ₂ : L ⊢! p ⋏ Γ.conj' ⟶ ⊥
hΔ₂ : L ⊢! ~p ⋏ Δ.conj' ⟶ ⊥
this✝ : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
this : L ⊬! (Γ ++ Δ).conj' ⟶ ⊥
⊢ ∀ (p : Formula α), p ∈ Γ ∨ p ∈ Δ → p ∈ T