intro v hv
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
xs : Set ν
xs' : Finset ν
τ' : PropAssignment ν
h : Disjoint xs ↑xs'
⊢ agreeOn xs (setMany τ xs' τ') τ
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
xs : Set ν
xs' : Finset ν
τ' : PropAssignment ν
h : Disjoint xs ↑xs'
v : ν
hv : v ∈ xs
⊢ setMany τ xs' τ' v = τ v