Lemma jt :
  forall l h l' h' s1 s2,
    StepStar l h (Seq s1 s2) l' h' Skip ->
    exists l'' h'',
      StepStar l h s1 l'' h'' Skip /\
      StepStar l'' h'' s2 l' h' Skip.
Proof.
  intros.
  remember (Seq s1 s2) as s.
  remember Skip as s' in H.
  revert Heqs' s1 s2 Heqs.
  induction H; intros; subst.
  - discriminate.
  - inversion H; subst; clear H.
    + specialize (IHStepStar eq_refl s1' s2 eq_refl). firstorder.
      eexists. eexists. intuition econstructor; eauto.
    + eexists. eexists. intuition eauto. constructor.
Qed.