proposition: Lemma cross_relation : forall (P : network -> list (name * (input + list output)) -> Prop), P step_async_init [] -> (forall st st' tr ev, step_async_star step_async_init st tr -> P st tr -> step_async st st' ev -> P st' (tr ++ ev)) -> forall st tr, step_async_star step_async_init st tr -> P st tr.
proof: Proof. Proof using. intros. find_apply_lem_hyp refl_trans_1n_n1_trace. prep_induction H1. induction H1; intros; subst; eauto. eapply H3; eauto. - apply refl_trans_n1_1n_trace. auto. - apply IHrefl_trans_n1_trace; auto. Qed.
imports: Verdi(Verdi HandlerMonad) StructTact(Fin) Verdi(StatePacketPacketDecomposition)