for MS being satisfying_equiv MusicStruct
for a, b being Element of MS holds a,b equiv a,b