Instead of having connectives pvs0 and pvs1 we now have one connective pvs that is indexed by a Boolean.