simpa [hv] using this v
α : 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
this : ∀ (v : Valuation α), v ⊧ p ∨ ∃ q ∈ Γ, ¬v ⊧ q
⊢ ∃ q ∈ Γ, ¬v ⊧ q
no goals