have ⟨φ, h⟩ := Quotient.exists_rep φ
ν : Type u_1
τ : PropAssignment ν
φ : PropFun ν
⊢ eval τ (neg φ) = !eval τ φ
ν : Type u_1
τ : PropAssignment ν
φ✝ : PropFun ν
φ : PropForm ν
h : ⟦φ⟧ = φ✝
⊢ eval τ (neg φ✝) = !eval τ φ✝