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

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