proposition: Lemma sos_sequence_aux : forall r i is r', sos_star r i is r' -> is = skip -> forall i' i'' r'', sos_star r' i' i'' r'' -> sos_star r (sequence i i') i'' r''.
proof: Proof. induction 1; intros; try (subst i); eauto. apply SOS7 with (r':=r')(i':=sequence i' i'0); auto. Qed.
imports: ZArith List syntax Lia