have l₄ : x ∈ generatedDisjunctions x := by 
  cases x
  case or f g => exact Or.inl rfl
  all_goals 
    exact rfl
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 = ∅
l₃ : isDisjunctionClosed (generatedDisjunctions 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 = ∅
l₃ : isDisjunctionClosed (generatedDisjunctions x)
l₄ : x ∈ generatedDisjunctions x
⊢ False