intro y hY
case a
ν : Type u_1
inst✝ : DecidableEq ν
b : Bool
x : ν
φ : PropForm ν
τ : PropAssignment ν
hNMem : x ∉ vars φ
⊢ PropAssignment.agreeOn (↑(vars φ)) (PropAssignment.set τ x b) τ
case a
ν : Type u_1
inst✝ : DecidableEq ν
b : Bool
x : ν
φ : PropForm ν
τ : PropAssignment ν
hNMem : x ∉ vars φ
y : ν
hY : y ∈ ↑(vars φ)
⊢ PropAssignment.set τ x b y = τ y