have ⟨⟨U,⟨prf₂⟩,l₁₀⟩,l₁₂⟩ := nonconstruction l₉
t u : Th
p : Pr
h₁✝ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₂ : ↑u ∩ Δ = ∅
P Q : Form
h₁ : P ∈ Δ ∧ Q ∈ Δ
h₂ : formalApplication (↑t) (▲{P¦Q}) ⊆ ↑↑p
R : Form
l₄ : ¬(R ∈ formalApplication (↑t) (▲{P}) → R ∈ ↑↑p)
S : Form
prf₁ : BProof {P} S
l₆ : S⊃R ∈ ↑t
l₈ : ¬R ∈ ↑↑p
T : Form
l₉ : ¬(T ∈ formalApplication (↑t) (▲{Q}) → T ∈ ↑↑p)
⊢ False
t u : Th
p : Pr
h₁✝ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₂ : ↑u ∩ Δ = ∅
P Q : Form
h₁ : P ∈ Δ ∧ Q ∈ Δ
h₂ : formalApplication (↑t) (▲{P¦Q}) ⊆ ↑↑p
R : Form
l₄ : ¬(R ∈ formalApplication (↑t) (▲{P}) → R ∈ ↑↑p)
S : Form
prf₁ : BProof {P} S
l₆ : S⊃R ∈ ↑t
l₈ : ¬R ∈ ↑↑p
T : Form
l₉ : ¬(T ∈ formalApplication (↑t) (▲{Q}) → T ∈ ↑↑p)
U : Form
prf₂ : BProof {Q} U
l₁₀ : U⊃T ∈ ↑t
l₁₂ : ¬T ∈ ↑↑p
⊢ False