have l₁ : ∀ g : Form, g ∈ generatedDisjunctions x → {g} ⊢ x := by
  intros g h₃
  induction g
  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 ⟩
  all_goals
    cases h₃; exact ⟨BProof.ax rfl⟩
case h
t : Th
x : Form
h₁ : x ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
h₂ : ¬x ∈ ↑t
⊢ False
case h
t : Th
x : Form
h₁ : x ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
h₂ : ¬x ∈ ↑t
l₁ : ∀ (g : Form), g ∈ generatedDisjunctions x → {g}⊢x
⊢ False