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