rcases this with ⟨⟨s₁, hs₁⟩, ⟨s₂, hs₂⟩⟩
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 Γ)
k : ℕ
r : L.Rel k
v : Fin k → SyntacticTerm L
h : ¬(rel r v ∉ ⛓️ ∨ nrel r v ∉ ⛓️)
this : (∃ s₁, rel r v ∈ ⛓️[s₁]) ∧ ∃ s₂, nrel r v ∈ ⛓️[s₂]
⊢ False
case intro.intro.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 Γ)
k : ℕ
r : L.Rel k
v : Fin k → SyntacticTerm L
h : ¬(rel r v ∉ ⛓️ ∨ nrel r v ∉ ⛓️)
s₁ : ℕ
hs₁ : rel r v ∈ ⛓️[s₁]
s₂ : ℕ
hs₂ : nrel r v ∈ ⛓️[s₂]
⊢ False