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.

What exactly are you not happy about? That the proofs are not as nice as they could be (for example, that they explicitly use automatically generated names and instantiate), or something more fundamental?

Yes, I referring to the ugliness of the proofs.

Ok, I can refactor them.

Nice, for a moment I was worried that this wouldn't actually hold constructively :)

Status changed to closed

Refactored, see 9c5a95d3. Thanks for the merge request.