case or Δ p q d ih =>
  simpa[or_assoc] using ih
α : Type u_1
Δ✝ : Sequent α
v : Valuation α
Δ : List (Formula α)
p q : Formula α
d : Derivation (p :: q :: Δ)
ih : v ⊧ (p :: q :: Δ).disj
⊢ v ⊧ (p ⋎ q :: Δ).disj
no goals