have := semVars'_subset_vars φ
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropForm ν
⊢ semVars ⟦φ⟧ ⊆ PropForm.vars φ
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropForm ν
this : LeanSAT.Model.PropFun.semVars' ⟦φ⟧ ⊆ ↑(PropForm.vars φ)
⊢ semVars ⟦φ⟧ ⊆ PropForm.vars φ