proposition: Lemma step_failure_star_lb_step_execution : forall s, event_step_star step_failure step_failure_init (hd s) -> lb_step_execution lb_step_failure s -> always (now (event_step_star step_failure step_failure_init)) s.
proof: Proof. Proof using. apply: step_star_lb_step_execution. exact: step_failure_star_lb_step_reachable. Qed.
imports: Verdi(Verdi) InfSeqExt(infseq exteq) Verdi(Ssrexport)