intro h
ν : Type u_1
inst✝ : DecidableEq ν
τ✝ : PropAssignment ν
x y : ν
τ : PropAssignment ν
v : Bool
⊢ x ≠ y → set τ x v y = τ y
ν : Type u_1
inst✝ : DecidableEq ν
τ✝ : PropAssignment ν
x y : ν
τ : PropAssignment ν
v : Bool
h : x ≠ y
⊢ set τ x v y = τ y