case inr h₄ =>
  have ⟨prf₁⟩ := ih₁ h₄.left
  have ⟨prf₂⟩ := ih₂ h₄.right
  have thm₁ := BTheorem.mp (BTheorem.adj prf₁.toTheorem prf₂.toTheorem) BTheorem.orE
  exact ⟨thm₁.toProof ⟩
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
no goals