Added definitions and facts about the concrete arrival sequence, used in Poet to generate assumption-less certificates