refine ⟨⟨⟨lindenbaumExtension u Δ, lindenbaumIsFormal⟩, lindenbaumIsPrime⟩, lindenbaumExtensionExtends, ?_⟩
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₄ : lindenbaumExtension u Δ ∩ Δ = ∅
⊢ ∃ r, u ≤ ↑r ∧ formalApplication ↑t ↑↑r ⊆ ↑↑p
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (↑t) (▲{f}) ⊆ ↑↑p }
l₄ : lindenbaumExtension u Δ ∩ Δ = ∅
⊢ formalApplication ↑t
      ↑↑{
            val :=
              { val := lindenbaumExtension u Δ,
                property := (_ : ∀ {f : Form}, f ∈ lindenbaumExtension u Δ ↔ lindenbaumExtension u Δ⊢f) },
            property :=
              (_ :
                ∀ {f g : Form},
                  f¦g ∈ lindenbaumExtension u Δ → f ∈ lindenbaumExtension u Δ ∨ g ∈ lindenbaumExtension u Δ) } ⊆
    ↑↑p