. apply semVars_impl
case hs
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
⊢ semVars (φ₁ ⇨ φ₂) ⊆ semVars φ₁ ∪ semVars φ₂

case a
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
⊢ semVars (φ₂ ⇨ φ₁) ⊆ semVars φ₁ ∪ semVars φ₂
case a
ν : Type u_1
inst✝ : DecidableEq ν
φ₁ φ₂ : PropFun ν
⊢ semVars (φ₂ ⇨ φ₁) ⊆ semVars φ₁ ∪ semVars φ₂