simp only [Finset.mem_union, mem_semVars]
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
x : ν
⊢ x ∈ semVars (φ₁ ⊔ φ₂) → x ∈ semVars φ₁ ∪ semVars φ₂
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
x : ν
⊢ (∃ τ, τ ⊨ φ₁ ⊔ φ₂ ∧ ¬(PropAssignment.set τ x !τ x) ⊨ φ₁ ⊔ φ₂) →
    (∃ τ, τ ⊨ φ₁ ∧ ¬(PropAssignment.set τ x !τ x) ⊨ φ₁) ∨ ∃ τ, τ ⊨ φ₂ ∧ ¬(PropAssignment.set τ x !τ x) ⊨ φ₂