proposition: Lemma sos_sequence_assoc_aux : forall r r' i i', sos_star r i i' r' -> i' = skip -> forall i1 i2 i3, i = (sequence i1 (sequence i2 i3)) -> sos_star r (sequence (sequence i1 i2) i3) skip r'.
proof: Proof. induction 1; intros; subst; try discriminate. match goal with id : sos_step _ _ _ _ |- _ => inversion id; subst; eauto end. match goal with id : sos_star _ _ _ _ |- _ => apply SOS7 with (2:=id);auto end. apply SOS7 with (i':=sequence (sequence i1' i2) i3)(r':=r'); auto. Qed.
imports: ZArith List syntax Lia