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

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