Make validity of STS fragments require a witness.

This commit changes the validity of STS fragments from S ≠ ∅ to ∃ s, s ∈ S.

I am not very happy with the changes to algebra/sts.v but I have more critical things to worry about at the moment.