proposition: Lemma sos_sequence : forall r r' r'' i i', sos_star r i skip r' -> sos_star r' i' skip r'' -> sos_star r (sequence i i') skip r''.
proof: Proof. intros; eapply sos_sequence_aux; eauto. Qed.
imports: ZArith List syntax Lia