implement equivalent sorts

Very crude first implementation. Some tests are expected to fail. Not ready for merge.

@yilongli @andreistefanescu can you have a look?
This is not enough, I think. For example, you have ```syntax A ::= X | Y``` and ```syntax KResult ::= X | Y```, you have to somehow compare the subsorts of A with subsorts of KResult to conclude that they are equivalent sorts. I don't think such information is already computed in context?