have l₁₄ : S¦U ∈ ▲{P¦Q} := ⟨(BTheorem.orFunctor prf₁.toTheorem prf₂.toTheorem).toProof⟩
case a
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₂ : ↑u ∩ Δ = ∅
P Q R S : Form
prf₁ : BProof {P} S
l₆ : S⊃R ∈ ↑t
T U : Form
prf₂ : BProof {Q} U
l₁₀ : U⊃T ∈ ↑t
⊢ R¦T ∈ formalApplication (↑t) (▲{P¦Q})
case a
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₂ : ↑u ∩ Δ = ∅
P Q R S : Form
prf₁ : BProof {P} S
l₆ : S⊃R ∈ ↑t
T U : Form
prf₂ : BProof {Q} U
l₁₀ : U⊃T ∈ ↑t
l₁₄ : S¦U ∈ ▲{P¦Q}
⊢ R¦T ∈ formalApplication (↑t) (▲{P¦Q})