simp only [Finset.mem_union, mem_semVars, satisfies_conj, not_and_or]
ν : 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) ⊨ φ₁) ∨ ∃ τ, τ ⊨ φ₂ ∧ ¬(PropAssignment.set τ x !τ x) ⊨ φ₂