Make it possible to make direct proofs not only as ts1,ts2,ts3,...,tsn, but also ts1 == tsn, ts2 =ts(n-1),..., tsi == tsi