proposition: Lemma lb_step_execution_invar : forall step x s, lb_step_execution step (Cons x s) -> lb_step_execution step s.
proof: Proof. Proof using. intros step x s e. change (lb_step_execution step (tl (Cons x s))). destruct e; simpl. assumption. Qed.
imports: Verdi(Verdi) InfSeqExt(infseq exteq) Verdi(Ssrexport)