Theorem: LeanSAT.Model.PropForm.semVars_subset_vars (LeanSAT/Model/PropVars.lean)

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

State before:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropForm ν
⊢ LeanSAT.Model.PropFun.semVars' ⟦φ⟧ ⊆ ↑(vars φ)
Tactic:
exact PropFun.semVars'_subset_vars φ
State after:
no goals