cases h
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
τ₁ τ₂ : SearchTree T Γ
h : Lt T Γ τ₂ τ₁
⊢ τ₂.seq ≺⟨τ₁.rank⟩ τ₁.seq
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
s✝ : ℕ
Δ₂✝ Δ₁✝ : Sequent L
a✝ : SearchTreeAux T Γ s✝ Δ₁✝
r✝ : Δ₂✝ ≺⟨s✝⟩ Δ₁✝
⊢ seq ⟨s✝ + 1, ⟨Δ₂✝, a✝.succ r✝⟩⟩ ≺⟨rank ⟨s✝, ⟨Δ₁✝, a✝⟩⟩⟩ seq ⟨s✝, ⟨Δ₁✝, a✝⟩⟩