Theorem: LeanSAT.Model.PropAssignment.agreeOn_set_of_not_mem (LeanSAT/Model/PropAssn.lean)

State before:
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
x : ν
X : Set ν
σ : PropAssignment ν
v : Bool
⊢ x ∉ X → agreeOn X (set σ x v) σ
Tactic:
aesop (add norm unfold agreeOn, norm unfold set)
State after:
no goals