Theorem: LeanSAT.Model.PropFun.eval_neg (LeanSAT/Model/PropFun.lean)

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

State before:
ν : Type u_1
τ : PropAssignment ν
φ✝ : PropFun ν
φ : PropForm ν
h : ⟦φ⟧ = φ✝
⊢ eval τ (neg φ✝) = !eval τ φ✝
Tactic:
simp [← h, eval, neg]
State after:
no goals