Theorem 6 requires that components share alphabets

Due to _**Theorem 6**. For any locally consistent specifications S, T and U over the same alphabet_ ...
we need to know the alphabet of all components before conjoining them. We currently don't have this information so we have to parse the model files (or hardcode it).

This means that Theorem6Conj1 and Theorem6Conj2 are implemented incorrectly, as they do not consider the alphabet. When the alphabets match we may be able to avoid the (currently) massive explosion in refinement checks as less combinations are possible.