intro u
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
p : SyntacticSemiformula L (0 + 1)
h : ∃' p ∈ ⛓️
⊢ ∀ (x : Model T Γ), ¬(Eval (Model.structure T Γ) ![x] Semiterm.fvar) p
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
p : SyntacticSemiformula L (0 + 1)
h : ∃' p ∈ ⛓️
u : Model T Γ
⊢ ¬(Eval (Model.structure T Γ) ![u] Semiterm.fvar) p