Theorem: LO.FirstOrder.Completeness.chain_spec (Logic/FirstOrder/Completeness/SearchTree.lean)

State before:
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 Γ)
s : ℕ
⊢ ⛓️[s + 1] ≺⟨s⟩ ⛓️[s]
Tactic:
simpa[chainU_val_fst_eq nwf s] using SearchTree.seq_of_lt (chainU_spec nwf s)
State after:
no goals