exact h₁ ⟨⟨r,h₂.right.right⟩,h₂.left⟩ h₂.right.left
t : Th
x : ℕ
h₁ : ∀ (p : Pr), t ≤ ↑p → x ∈ theoryValuation ↑p
r : Set Form
h₂ : r ∈ { p | isPrimeTheory p ∧ ↑t ≤ p ∧ formalTheory p }
⊢ #x ∈ r
no goals