Theorem: LeanSAT.Model.PropFun.satisfies_forallAssn (LeanSAT/Model/Quantifiers.lean)

State before:
ν' : Type u_2
inst✝ : Fintype ν'
ν : Type u_1
φ : PropFun ν
f : PropAssignment ν → PropAssignment ν'
τ : PropAssignment ν'
⊢ τ ⊨ forallAssn f φ ↔ ∀ (σ : PropAssignment ν), σ ⊨ φ → τ = f σ
Tactic:
simp [forallAssn]
State after:
no goals