proposition: Lemma lem_seq_comp : forall c1 c2 s1 s2 s3, (c1, s1) -->* (Nop, s2) -> (c2, s2) -->* (Nop, s3) -> (c1;; c2, s1) -->* (Nop, s3).
proof: Proof. intros c1 c2 s1 s2 s3 H1 H2. assert ((c1;; c2, s1) -->* (Nop;; c2, s2)) by sauto use: lem_star_seq2. sauto. Qed.
imports: Hammer(Tactics Reflect) String Arith Lia Relations