case or f g => exact Or.inl rfl
t : Th
f g : Form
h₁ : f¦g ∈ ⋂₀ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
h₂ : ¬f¦g ∈ ↑t
l₁ : ∀ (g_1 : Form), g_1 ∈ generatedDisjunctions (f¦g) → {g_1}⊢f¦g
l₂ : ↑t ∩ generatedDisjunctions (f¦g) = ∅
l₃ : isDisjunctionClosed (generatedDisjunctions (f¦g))
⊢ f¦g ∈ generatedDisjunctions (f¦g)
no goals