cases h₃
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
case impl.refl
t : Th
a✝¹ a✝ : Form
h₁ : a✝¹⊃a✝ ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
h₂ : ¬a✝¹⊃a✝ ∈ ↑t
a_ih✝¹ : a✝¹ ∈ generatedDisjunctions (a✝¹⊃a✝) → {a✝¹}⊢a✝¹⊃a✝
a_ih✝ : a✝ ∈ generatedDisjunctions (a✝¹⊃a✝) → {a✝}⊢a✝¹⊃a✝
⊢ {a✝¹⊃a✝}⊢a✝¹⊃a✝