Theorem: LeanSAT.Model.PropFun.satisfies_ofSet (LeanSAT/Model/OfFun.lean)

State before:
V : Type u_1
τ : PropAssignment V
inst✝² : DecidableEq V
inst✝¹ : Fintype V
S : Set (PropAssignment V)
inst✝ : DecidablePred fun x => x ∈ S
⊢ τ ⊨ ofSet S ↔ τ ∈ S
Tactic:
simp [ofSet]
State after:
no goals