proposition: Lemma step_star_lb_step_execution : forall lb_step step init, step_star_lb_step_reachable lb_step step init -> forall s, event_step_star step init (hd s) -> lb_step_execution lb_step s -> always (now (event_step_star step init)) s.
proof: Proof. Proof using. move => lb_step step init H_r. case => e s H_star. move: e s H_star. cofix cf. move => e. case => e' s H_star H_exec'. constructor; first by []. apply cf. inversion H_exec'; subst_max. simpl in *. rewrite /event_step_star /=. rewrite /event_step_star /= in H_star. rewrite /step_star_lb_step_reachable in H_r. have H_d := H_r _ _ _ _ _ H_star H2. rewrite H3. exact: H_r _ _ _ _ _ H_star H2. move: H_exec'. apply: lb_step_execution_invar. Qed.
imports: Verdi(Verdi) InfSeqExt(infseq exteq) Verdi(Ssrexport)