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