simp [SemanticEntails.entails, satisfies, ofFun]
V : Type u_1
inst✝¹ : DecidableEq V
inst✝ : Fintype V
p : PropAssignment V → Bool
τ : PropAssignment V
⊢ τ ⊨ ofFun p ↔ p τ = true
V : Type u_1
inst✝¹ : DecidableEq V
inst✝ : Fintype V
p : PropAssignment V → Bool
τ : PropAssignment V
⊢ eval τ (Fintype.elim_elems (fun L h1 x => ⟦PropForm.ofFun p L h1⟧) ⋯) = p τ