proposition: Lemma sos_sequence_assoc : forall r r' i1 i2 i3, sos_star r (sequence i1 (sequence i2 i3)) skip r' -> sos_star r (sequence (sequence i1 i2) i3) skip r'.
proof: Proof. intros; eapply sos_sequence_assoc_aux; eauto. Qed.
imports: ZArith List syntax Lia