case or f g ih₁ ih₂ =>
  cases h₃
  case inl h₄ => rw [h₄]; exact ⟨BProof.ax rfl⟩
  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₃ : f¦g ∈ generatedDisjunctions x
⊢ {f¦g}⊢x
no goals