have l₂ : ↑t ∩ generatedDisjunctions x = ∅ := by
  apply Set.eq_empty_iff_forall_not_mem.mpr
  intros y h₃
  have ⟨prf₁⟩ := l₁ y h₃.right
  exact h₂ (t.property.mpr ⟨BProof.monotone (Set.singleton_subset_iff.mpr h₃.left) prf₁⟩)
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
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
l₂ : ↑t ∩ generatedDisjunctions x = ∅
⊢ False