for p1, p2 being FinSequence st not p1,p2 are_c=-comparable holds
{p1,p2} is AntiChain_of_Prefixes-like