all_goals
  cases h₃; exact ⟨BProof.ax rfl⟩
case atom
t : Th
x : Form
h₁ : x ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
h₂ : ¬x ∈ ↑t
a✝ : ℕ
h₃ : #a✝ ∈ generatedDisjunctions x
⊢ {#a✝}⊢x

case neg
t : Th
x : Form
h₁ : x ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
h₂ : ¬x ∈ ↑t
a✝ : Form
a_ih✝ : a✝ ∈ generatedDisjunctions x → {a✝}⊢x
h₃ : ~a✝ ∈ generatedDisjunctions x
⊢ {~a✝}⊢x

case and
t : Th
x : Form
h₁ : x ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
h₂ : ¬x ∈ ↑t
a✝¹ a✝ : Form
a_ih✝¹ : a✝¹ ∈ generatedDisjunctions x → {a✝¹}⊢x
a_ih✝ : a✝ ∈ generatedDisjunctions x → {a✝}⊢x
h₃ : a✝¹&a✝ ∈ generatedDisjunctions x
⊢ {a✝¹&a✝}⊢x

case impl
t : Th
x : Form
h₁ : x ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
h₂ : ¬x ∈ ↑t
a✝¹ a✝ : Form
a_ih✝¹ : a✝¹ ∈ generatedDisjunctions x → {a✝¹}⊢x
a_ih✝ : a✝ ∈ generatedDisjunctions x → {a✝}⊢x
h₃ : a✝¹⊃a✝ ∈ generatedDisjunctions x
⊢ {a✝¹⊃a✝}⊢x
no goals