Theorem: LeanSAT.Model.PropForm.entails_ofFun (LeanSAT/Model/OfFun.lean)

State before:
V : Type u_1
inst✝ : DecidableEq V
L : List V
hc : ∀ (v : V), v ∈ L
p : PropAssignment V → Bool
τ : PropAssignment V
⊢ τ ⊨ ofFun p L hc ↔ p τ = true
Tactic:
simp [SemanticEntails.entails, satisfies]
State after:
no goals