have := semVars_disj (φ₁ᶜ) φ₂
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
⊢ semVars (φ₂ ⊔ φ₁ᶜ) ⊆ semVars φ₁ ∪ semVars φ₂
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
this : semVars (φ₁ᶜ ⊔ φ₂) ⊆ semVars φ₁ᶜ ∪ semVars φ₂
⊢ semVars (φ₂ ⊔ φ₁ᶜ) ⊆ semVars φ₁ ∪ semVars φ₂