Theorem: LeanSAT.Model.PropFun.mem_semVars (LeanSAT/Model/PropVars.lean)

State before:
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropFun ν
x : ν
⊢ x ∈ semVars φ ↔ ∃ τ, τ ⊨ φ ∧ (fun M φ => ¬M ⊨ φ) (PropAssignment.set τ x !τ x) φ
Tactic:
simp [Set.Finite.mem_toFinset, semVars, semVars']
State after:
no goals