have ⟨prf₁⟩ := ih₁ h₄.left
t : Th
x : Form
h₁ : x ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
h₂ : ¬x ∈ ↑t
f g : Form
ih₁ : f ∈ generatedDisjunctions x → {f}⊢x
ih₂ : g ∈ generatedDisjunctions x → {g}⊢x
h₄ : generatedDisjunctions x f ∧ generatedDisjunctions x g
⊢ {f¦g}⊢x
t : Th
x : Form
h₁ : x ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
h₂ : ¬x ∈ ↑t
f g : Form
ih₁ : f ∈ generatedDisjunctions x → {f}⊢x
ih₂ : g ∈ generatedDisjunctions x → {g}⊢x
h₄ : generatedDisjunctions x f ∧ generatedDisjunctions x g
prf₁ : BProof {f} x
⊢ {f¦g}⊢x