all_goals 
  exact rfl
case atom
t : Th
a✝ : ℕ
h₁ : #a✝ ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
h₂ : ¬#a✝ ∈ ↑t
l₁ : ∀ (g : Form), g ∈ generatedDisjunctions #a✝ → {g}⊢#a✝
l₂ : ↑t ∩ generatedDisjunctions #a✝ = ∅
l₃ : isDisjunctionClosed (generatedDisjunctions #a✝)
⊢ #a✝ ∈ generatedDisjunctions #a✝

case neg
t : Th
a✝ : Form
h₁ : ~a✝ ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
h₂ : ¬~a✝ ∈ ↑t
l₁ : ∀ (g : Form), g ∈ generatedDisjunctions ~a✝ → {g}⊢~a✝
l₂ : ↑t ∩ generatedDisjunctions ~a✝ = ∅
l₃ : isDisjunctionClosed (generatedDisjunctions ~a✝)
⊢ ~a✝ ∈ generatedDisjunctions ~a✝

case and
t : Th
a✝¹ a✝ : Form
h₁ : a✝¹&a✝ ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
h₂ : ¬a✝¹&a✝ ∈ ↑t
l₁ : ∀ (g : Form), g ∈ generatedDisjunctions (a✝¹&a✝) → {g}⊢a✝¹&a✝
l₂ : ↑t ∩ generatedDisjunctions (a✝¹&a✝) = ∅
l₃ : isDisjunctionClosed (generatedDisjunctions (a✝¹&a✝))
⊢ a✝¹&a✝ ∈ generatedDisjunctions (a✝¹&a✝)

case impl
t : Th
a✝¹ a✝ : Form
h₁ : a✝¹⊃a✝ ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
h₂ : ¬a✝¹⊃a✝ ∈ ↑t
l₁ : ∀ (g : Form), g ∈ generatedDisjunctions (a✝¹⊃a✝) → {g}⊢a✝¹⊃a✝
l₂ : ↑t ∩ generatedDisjunctions (a✝¹⊃a✝) = ∅
l₃ : isDisjunctionClosed (generatedDisjunctions (a✝¹⊃a✝))
⊢ a✝¹⊃a✝ ∈ generatedDisjunctions (a✝¹⊃a✝)
no goals