intro x
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
⊢ semVars (φ₁ ⊔ φ₂) ⊆ semVars φ₁ ∪ semVars φ₂
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
x : ν
⊢ x ∈ semVars (φ₁ ⊔ φ₂) → x ∈ semVars φ₁ ∪ semVars φ₂