proposition: Lemma simulation : forall net tr, step_async_star step_async_init net tr -> step_1_star init (revert_state net) (revert_trace tr).
proof: Proof. Proof using. intros. apply refl_trans_1n_n1_trace in H. prep_induction H. induction H; intros; subst. - unfold step_async_init, revert_state. constructor. - repeat concludes. rewrite revert_trace_app. unfold step_1_star. find_apply_lem_hyp inductive_simulation. simpl in *. unfold step_1_star in *. eauto using refl_trans_1n_trace_trans. Qed.
imports: Verdi(Verdi HandlerMonad)