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