proposition: Lemma step_async_star_lb_step_reachable : step_star_lb_step_reachable lb_step_async step_async step_async_init.
proof: Proof. Proof using. rewrite /step_star_lb_step_reachable. move => net l. move => net' tr tr' H_star H_st. invcs H_st. - set net' := {| nwPackets := _ ; nwState := _ |}. apply (@refl_trans_1n_trace_trans _ _ _ _ net) => //. have ->: [(pDst p, inr out)] = [(pDst p, inr out)] ++ [] by []. apply: (@RT1nTStep _ _ _ _ net'); last exact: RT1nTBase. apply: (@StepAsync_deliver _ _ _ _ _ xs ys _ d l0) => //. rewrite /net_handlers /= /unlabeled_net_handlers /=. repeat break_let. by tuple_inversion. - set net' := {| nwPackets := _ ; nwState := _ |}. apply (@refl_trans_1n_trace_trans _ _ _ _ net) => //. have ->: [(h, inl inp); (h, inr out)] = [(h, inl inp); (h, inr out)] ++ [] by []. apply: (@RT1nTStep _ _ _ _ net'); last exact: RT1nTBase. apply: StepAsync_input => //. rewrite /input_handlers /= /unlabeled_input_handlers /=. repeat break_let. by tuple_inversion. - by have ->: tr' ++ [] = tr' by auto with datatypes. Qed.
imports: Verdi(Verdi) InfSeqExt(infseq exteq) Verdi(Ssrexport)