simp[List.map_disj]
α : Type u_1
Δ✝ : Sequent α
v : Valuation α
Δ : List (Formula α)
a : α
⊢ v ⊧ (Formula.atom a :: Formula.natom a :: Δ).disj
α : Type u_1
Δ✝ : Sequent α
v : Valuation α
Δ : List (Formula α)
a : α
⊢ v.val a ∨ ¬v.val a ∨ ∃ p ∈ Δ, v ⊧ p