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.
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.