Theorem: LO.FirstOrder.Completeness.Redux.antimonotone (Logic/FirstOrder/Completeness/SearchTree.lean)

State before:
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
c : Code L
Δ₂ Δ₁ : Sequent L
h : Δ₂ ≺[c] Δ₁
⊢ Δ₁ ⊆ Δ₂
Tactic:
cases h <;> simp[List.subset_cons_of_subset _ (List.subset_cons _ _)]
State after:
no goals