case and₁ =>
  exact Or.inl (Set.mem_iUnion.mpr ⟨(encode $ Code.and p q).pair s + 1, by simp[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 ∈ ⛓️
s : ℕ
hs : p ⋏ q ∈ ⛓️[s]
a✝ : p ⋏ q ∈ ⛓️[(encode (Code.and p q)).pair s]
hΔ : ⛓️[(encode (Code.and p q)).pair s + 1] = p :: ⛓️[(encode (Code.and p q)).pair s]
⊢ p ∈ ⛓️ ∨ q ∈ ⛓️
no goals