have : ∃ p ∈ Δ, v ⊧ p := by simpa [List.map_disj] using ih
α : Type u_1
Δ✝ : Sequent α
v : Valuation α
Δ Γ : Sequent α
a✝ : Derivation Δ
ss : Δ ⊆ Γ
ih : v ⊧ List.disj Δ
⊢ v ⊧ List.disj Γ
α : Type u_1
Δ✝ : Sequent α
v : Valuation α
Δ Γ : Sequent α
a✝ : Derivation Δ
ss : Δ ⊆ Γ
ih : v ⊧ List.disj Δ
this : ∃ p ∈ Δ, v ⊧ p
⊢ v ⊧ List.disj Γ