case wk Δ Γ _ ss ih =>
  have : ∃ p ∈ Δ, v ⊧ p := by simpa [List.map_disj] using ih
  rcases this with ⟨p, hp, hvp⟩
  simp [List.map_disj]; exact ⟨p, ss hp, hvp⟩
α : Type u_1
Δ✝ : Sequent α
v : Valuation α
Δ Γ : Sequent α
a✝ : Derivation Δ
ss : Δ ⊆ Γ
ih : v ⊧ List.disj Δ
⊢ v ⊧ List.disj Γ
no goals