Theorem: LeanSAT.Model.PropFun.satisfies_var (LeanSAT/Model/PropFun.lean)

State before:
ν : Type u_1
τ : PropAssignment ν
x : ν
⊢ τ ⊨ var x ↔ τ x = true
Tactic:
simp [sEntails, satisfies]
State after:
no goals