Valid arrival sequence

Currently a lot of files use two hypotheses

Hypothesis H_arrival_times_are_consistent : consistent_arrival_times arr_seq.
Hypothesis H_arr_seq_is_a_set : arrival_sequence_uniq arr_seq.

instead of the combined valid_arrival_sequence.

This MR aims to fix this.