simp only [PropFun.semVars, Set.Finite.toFinset_subset]
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropForm ν
⊢ PropFun.semVars ⟦φ⟧ ⊆ vars φ
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropForm ν
⊢ LeanSAT.Model.PropFun.semVars' ⟦φ⟧ ⊆ ↑(vars φ)