In course material for semantics of programming languages the definition of sos_step expresses that skip (which is the equivalent of your term) is ignored when executed at the first step of a sequence. Then, the statement you wish to obtain is a consequence of associativity of sequence with respect to executions as expressed by theorem sos_sequence_aux.