exact ih.inv (SearchTree.Lt.intro a r)
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 Γ)
A : Acc (SearchTree.Lt T Γ) ⊤
s✝ : ℕ
Δ : Sequent L
s : ℕ
Δ₁ Δ₂ : Sequent L
a : SearchTreeAux T Γ s Δ₁
r : Δ₂ ≺⟨s⟩ Δ₁
ih : Acc (SearchTree.Lt T Γ) ⟨s, ⟨Δ₁, a⟩⟩
⊢ Acc (SearchTree.Lt T Γ) ⟨s + 1, ⟨Δ₂, a.succ r⟩⟩
no goals