rcases this
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₂]
this✝ : rel r v ∈ ⛓️[(encode (Code.axL r v)).pair (max s₁ s₂)] ∧ nrel r v ∈ ⛓️[(encode (Code.axL r v)).pair (max s₁ s₂)]
Δ' : Sequent L
this : Δ' ≺[Code.axL r v] ⛓️[(encode (Code.axL r v)).pair (max s₁ s₂)]
⊢ rel r v ∉ ⛓️[(encode (Code.axL r v)).pair (max s₁ s₂)] ∨ nrel r v ∉ ⛓️[(encode (Code.axL r v)).pair (max s₁ s₂)]
case axLRefl
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₂]
this : rel r v ∈ ⛓️[(encode (Code.axL r v)).pair (max s₁ s₂)] ∧ nrel r v ∈ ⛓️[(encode (Code.axL r v)).pair (max s₁ s₂)]
a✝ : rel r v ∉ ⛓️[(encode (Code.axL r v)).pair (max s₁ s₂)] ∨ nrel r v ∉ ⛓️[(encode (Code.axL r v)).pair (max s₁ s₂)]
⊢ rel r v ∉ ⛓️[(encode (Code.axL r v)).pair (max s₁ s₂)] ∨ nrel r v ∉ ⛓️[(encode (Code.axL r v)).pair (max s₁ s₂)]