have : 𝓓 ⊬! (Γ₁ ++ Γ₂).conj' ⟶ (Δ₁ ++ Δ₂).disj' := hCon (by simp; rintro q (hq₁ | hq₂); exact hΓ₁ q hq₁; exact hΓ₂ q hq₂) (by simp; rintro q (hq₁ | hq₂); exact hΔ₁ q hq₁; exact hΔ₂ q hq₂)
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
p : Formula α
hC : ¬(𝓓)-Consistent (insert p t.1, t.2) ∧ ¬(𝓓)-Consistent (t.1, insert p t.2)
hC₁ : ¬(𝓓)-Consistent (insert p t.1, t.2)
hC₂ : ¬(𝓓)-Consistent (t.1, insert p t.2)
Γ₁ Δ₁ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ₁, p ∈ t.1
hΔ₁ : ∀ p ∈ Δ₁, p ∈ t.2
h₁ : 𝓓 ⊢! Γ₁.conj' ⋏ p ⟶ Δ₁.disj'
Γ₂ Δ₂ : List (Formula α)
hΓ₂ : ∀ p ∈ Γ₂, p ∈ t.1
hΔ₂ : ∀ p ∈ Δ₂, p ∈ t.2
h₂ : 𝓓 ⊢! Γ₂.conj' ⟶ p ⋎ Δ₂.disj'
this : 𝓓 ⊢! (Γ₁ ++ Γ₂).conj' ⟶ (Δ₁ ++ Δ₂).disj'
⊢ False
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
t : Tableau α
inst✝² : DecidableEq α
inst✝¹ : Inhabited α
𝓓 : DeductionParameter α
inst✝ : 𝓓.IncludeEFQ
hCon : (𝓓)-Consistent t
p : Formula α
hC : ¬(𝓓)-Consistent (insert p t.1, t.2) ∧ ¬(𝓓)-Consistent (t.1, insert p t.2)
hC₁ : ¬(𝓓)-Consistent (insert p t.1, t.2)
hC₂ : ¬(𝓓)-Consistent (t.1, insert p t.2)
Γ₁ Δ₁ : List (Formula α)
hΓ₁ : ∀ p ∈ Γ₁, p ∈ t.1
hΔ₁ : ∀ p ∈ Δ₁, p ∈ t.2
h₁ : 𝓓 ⊢! Γ₁.conj' ⋏ p ⟶ Δ₁.disj'
Γ₂ Δ₂ : List (Formula α)
hΓ₂ : ∀ p ∈ Γ₂, p ∈ t.1
hΔ₂ : ∀ p ∈ Δ₂, p ∈ t.2
h₂ : 𝓓 ⊢! Γ₂.conj' ⟶ p ⋎ Δ₂.disj'
this✝ : 𝓓 ⊢! (Γ₁ ++ Γ₂).conj' ⟶ (Δ₁ ++ Δ₂).disj'
this : 𝓓 ⊬! (Γ₁ ++ Γ₂).conj' ⟶ (Δ₁ ++ Δ₂).disj'
⊢ False