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

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