simpa [Semantics.Valid, List.map_disj] using Derivation.sound (Tait.ofConsRight d)
α : Type u_1
Δ : Sequent α
T : Theory α
p : Formula α
Γ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ T
d : Γ ⊢² [p]
v : Valuation α
hT : v ∈ Semantics.models (Valuation α) T
hv : ¬v ⊧ p
⊢ ∀ (v : Valuation α), v ⊧ p ∨ ∃ q ∈ Γ, ¬v ⊧ q
no goals