proposition: Lemma lem_star_seq2 : forall c1 c2 s c1' s', (c1, s) -->* (c1', s') -> (c1;; c2, s) -->* (c1';; c2, s').
proof: Proof. enough (forall p1 p2, p1 -->* p2 -> forall c1 c2 s c1' s', p1 = (c1, s) -> p2 = (c1', s') -> (c1;; c2, s) -->* (c1';; c2, s')). { eauto. } induction 1; sauto lq: on. Qed.
imports: Hammer(Tactics Reflect) String Arith Lia Relations