rcases this with (h | 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
nwf : ¬WellFounded (SearchTree.Lt T Γ)
p q : SyntacticFormula L
h : p ⋏ q ∈ ⛓️
a✝¹ : (Evalf (Model.structure T Γ) Semiterm.fvar) p
a✝ : (Evalf (Model.structure T Γ) Semiterm.fvar) q
this : p ∈ ⛓️ ∨ q ∈ ⛓️
⊢ False
case inl
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 q : SyntacticFormula L
h✝ : p ⋏ q ∈ ⛓️
a✝¹ : (Evalf (Model.structure T Γ) Semiterm.fvar) p
a✝ : (Evalf (Model.structure T Γ) Semiterm.fvar) q
h : p ∈ ⛓️
⊢ False

case inr
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 q : SyntacticFormula L
h✝ : p ⋏ q ∈ ⛓️
a✝¹ : (Evalf (Model.structure T Γ) Semiterm.fvar) p
a✝ : (Evalf (Model.structure T Γ) Semiterm.fvar) q
h : q ∈ ⛓️
⊢ False