proposition: Lemma lb_step_execution_extensional : forall step, extensional (lb_step_execution step).
proof: Proof. Proof using. move => step. rewrite /extensional /=. cofix c. case => e1; case => e1' s1. case => e2; case => e2' s2 H_eq. find_apply_lem_hyp exteq_inversion. break_and. find_copy_apply_lem_hyp exteq_inversion. break_and. repeat find_rewrite. move => H_exec. inversion H_exec; subst. apply (Cons_lb_step_exec _ tr) => //. by apply: c; eauto. Qed.
imports: Verdi(Verdi) InfSeqExt(infseq exteq) Verdi(Ssrexport)