have : v ⊧ q := by simpa[hv] using ihq
case neg
α : Type u_1
Δ✝ : Sequent α
v : Valuation α
Δ : List (Formula α)
p q : Formula α
a✝¹ : Derivation (p :: Δ)
a✝ : Derivation (q :: Δ)
ihp : v ⊧ (p :: Δ).disj
ihq : v ⊧ (q :: Δ).disj
hv : ¬v ⊧ Δ.disj
this : v ⊧ p
⊢ v ⊧ (p ⋏ q :: Δ).disj
case neg
α : Type u_1
Δ✝ : Sequent α
v : Valuation α
Δ : List (Formula α)
p q : Formula α
a✝¹ : Derivation (p :: Δ)
a✝ : Derivation (q :: Δ)
ihp : v ⊧ (p :: Δ).disj
ihq : v ⊧ (q :: Δ).disj
hv : ¬v ⊧ Δ.disj
this✝ : v ⊧ p
this : v ⊧ q
⊢ v ⊧ (p ⋏ q :: Δ).disj