exact ⟨BProof.ax rfl⟩
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✝
no goals