generalize hΔ : ⛓️[(encode $ Code.ex p t).pair s + 1] = Δ at this
case intro
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 1
h : ∃' p ∈ ⛓️
t : Semiterm L ℕ 0
s : ℕ
hs : ∃' p ∈ ⛓️[s]
this : ⛓️[(encode (Code.ex p t)).pair s + 1] ≺[Code.ex p t] ⛓️[(encode (Code.ex p t)).pair s]
⊢ [→ t].hom p ∈ ⛓️
case intro
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 1
h : ∃' p ∈ ⛓️
t : Semiterm L ℕ 0
s : ℕ
hs : ∃' p ∈ ⛓️[s]
Δ : Sequent L
hΔ : ⛓️[(encode (Code.ex p t)).pair s + 1] = Δ
this : Δ ≺[Code.ex p t] ⛓️[(encode (Code.ex p t)).pair s]
⊢ [→ t].hom p ∈ ⛓️