intro hNMem
ν : Type u_1
inst✝ : DecidableEq ν
b : Bool
x : ν
φ : PropForm ν
τ : PropAssignment ν
⊢ x ∉ vars φ → eval (PropAssignment.set τ x b) φ = eval τ φ
ν : Type u_1
inst✝ : DecidableEq ν
b : Bool
x : ν
φ : PropForm ν
τ : PropAssignment ν
hNMem : x ∉ vars φ
⊢ eval (PropAssignment.set τ x b) φ = eval τ φ