have l₄ := formalAppMonotoneRight ↑u l₃
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (▲{f}) ↑u ⊆ ↑↑p }
P : Form
h₂ : P ∈ ↑t ∩ Δ
l₃ : ▲{P} ⊆ ↑t
⊢ False
t u : Th
p : Pr
h₁ : formalApplicationFunction t u ≤ ↑p
Δ : Set Form := { f | ¬formalApplication (▲{f}) ↑u ⊆ ↑↑p }
P : Form
h₂ : P ∈ ↑t ∩ Δ
l₃ : ▲{P} ⊆ ↑t
l₄ : flip formalApplication (↑u) (▲{P}) ≤ flip formalApplication ↑u ↑t
⊢ False