Theorem: LeanSAT.Model.PropPred.satisfies_def (LeanSAT/Model/PropPred.lean)

State before:
ν : Type u_1
τ : PropAssignment ν
f : PropPred ν
⊢ τ ⊨ f ↔ f τ
Tactic:
rfl
State after:
no goals